let X be set ; :: thesis: meet X c= union X

A1: now :: thesis: ( X <> {} implies meet X c= union X )

assume A2: X <> {} ; :: thesis: meet X c= union X

now :: thesis: for x being object st x in meet X holds
x in union X

set y = the Element of X;
let x be object ; :: thesis: ( x in meet X implies x in union X )
assume x in meet X ; :: thesis: x in union X
then x in the Element of X by A2, Def1;
hence x in union X by A2, TARSKI:def 4; :: thesis: verum

end;

hence meet X c= union X ; :: thesis: verum

end;

( X = {} implies meet X c= union X ) by Def1;
hence meet X c= union X by A1; :: thesis: verum