For instance, let us assume that we want to demonstrate p & q & r. At this point, the following demonstrations can also be done.
p & q & r
proof
......
thus p;
......
thus q;
......
thus r;
end;
First, let us assume that p could be demonstrated and it becomes thus p. Also, continuing with the demonstration, it becomes thus q, when we demonstrate even further, it becomes thus r. In this case, the Mizar system looks for thus .... . For this, three thus appear so that of a proposition p & q & r that should be demonstrated first, we will recognize the fact that p could be demonstrated. Also, we will recognize that the second one could be demonstrated with thus q. Finally, we will be aware that everything could be demonstrated with thus r. The end can also be stated as thus theses. In this case, system and p,q are already demonstrated and only r is left; therefore, we will recognize that r is the thesis. In this way, we will be aware that thus thesis is thus r. It is fine to write either one of them.
In addition, when demonstrating p & q & r, we can either demonstrate p first then q & r next, or p & q first and r later. We can demonstrate by dividing freely.