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

A1: now

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

now

set y = the Element of X;
let x be set ; :: 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 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