per cases ( not X is empty or X is empty ) ;
case not X is empty ; :: thesis: ex b1 being set st
for b2 being set st b2 in X holds
b2 in b1
take X ; :: thesis: for b1 being set st b1 in X holds
b1 in X
thus for b1 being set st b1 in X holds
b1 in X ; :: thesis: verum
end;
case X is empty ; :: thesis: ex b1 being set st
for b2 being set st b2 is empty holds
b2 in b1
take {{}} ; :: thesis: for b1 being set st b1 is empty holds
b1 in {{}}
let y be set ; :: thesis: ( y is empty implies y in {{}} )
thus ( y is empty implies y in {{}} ) by TARSKI:def 1; :: thesis: verum
end;
end;