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

A1: now

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

now

let x be set ; :: thesis: ( x in meet X implies x in union X )
assume A3: x in meet X ; :: thesis: x in union X
consider y being Element of X;
x in y by A2, A3, Def1;
hence x in union X by A2, TARSKI:def 4; :: thesis: verum

end;

hence meet X c= union X by TARSKI:def 3; :: thesis: verum

end;

now

assume X = {} ; :: thesis: meet X c= union X
then meet X = {} by Def1;
hence meet X c= union X by XBOOLE_1:2; :: thesis: verum

end;

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