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

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

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

( X = {} implies meet X c= union X )
by Def1;assume A2:
X <> {}
; :: thesis: meet X c= union X

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

x in union X

hence
meet X c= union X
; :: thesis: verumx 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;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

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