たとえば，p & q & r を証明したいとします．このとき，次のように証明することも出来ます．
p & q & r
proof
......
thus p;
......
thus q;
......
thus r;
end;
まず p が証明できたとします．そうすると thus p となります．また証明を続けて thus q， さらに証明していって thus r ．この場合 Mizar のシステムは，thus ...を捜します．これには thus が3つもでてきますので，最初の thus p で証明すべき命題 p & q & r のうちの
p が証明できたということを認識し，次に thus q で２番目も証明できたことを認識します．最後に thus r ですべて証明されたことを認識します．最後は thus thesis とすることもできます．この場合，システムは既に
p,q はすでに証明されていて，残っているのは r だけで，r が thesis だと認識します．こうして，thus thesis は thus r であるということを認識します．どちらを書いてもかまいません．
それから，p & q & r を証明するときに，p を先に証明し，q & r を後に証明したり，あるいは p & q を先に証明し，r を後に証明してもかまいません．自由に分割して証明することができます．