let D be set ; :: thesis: for F being Subset-Family of D st F <> {} holds
union (COMPLEMENT F) = ([#] D) \ (meet F)
let F be Subset-Family of D; :: thesis: ( F <> {} implies union (COMPLEMENT F) = ([#] D) \ (meet F) )
assume A1: F <> {} ; :: thesis: union (COMPLEMENT F) = ([#] D) \ (meet F)
A2: ([#] D) \ (meet F) c= union (COMPLEMENT F)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ([#] D) \ (meet F) or x in union (COMPLEMENT F) )
assume A3: x in ([#] D) \ (meet F) ; :: thesis: x in union (COMPLEMENT F)
then not x in meet F by XBOOLE_0:def 5;
then consider X being set such that
A4: X in F and
A5: not x in X by A1, Def1;
reconsider X = X as Subset of D by A4;
reconsider XX = X ` as set ;
A6: (X `) ` = X ;
ex Y being set st
( x in Y & Y in COMPLEMENT F )

proof

take XX ; :: thesis: ( x in XX & XX in COMPLEMENT F )
thus ( x in XX & XX in COMPLEMENT F ) by A3, A4, A5, A6, Def7, XBOOLE_0:def 5; :: thesis: verum

end;

hence x in union (COMPLEMENT F) by TARSKI:def 4; :: thesis: verum

end;

union (COMPLEMENT F) c= ([#] D) \ (meet F)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (COMPLEMENT F) or x in ([#] D) \ (meet F) )
assume A7: x in union (COMPLEMENT F) ; :: thesis: x in ([#] D) \ (meet F)
then consider X being set such that
A8: x in X and
A9: X in COMPLEMENT F by TARSKI:def 4;
reconsider X = X as Subset of D by A9;
reconsider XX = X ` as set ;
ex Y being set st
( Y in F & not x in Y )

proof

take Y = XX; :: thesis: ( Y in F & not x in Y )
thus Y in F by A9, Def7; :: thesis: not x in Y
thus not x in Y by A8, XBOOLE_0:def 5; :: thesis: verum

end;

then not x in meet F by Def1;
hence x in ([#] D) \ (meet F) by A7, XBOOLE_0:def 5; :: thesis: verum

end;

hence union (COMPLEMENT F) = ([#] D) \ (meet F) by A2; :: thesis: verum