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)

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

union (COMPLEMENT F) c= ([#] D) \ (meet F)
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 )

end;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

hence
x in union (COMPLEMENT F)
by TARSKI:def 4; :: thesis: verum
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;thus ( x in XX & XX in COMPLEMENT F ) by A3, A4, A5, A6, Def7, XBOOLE_0:def 5; :: thesis: verum

proof

hence
union (COMPLEMENT F) = ([#] D) \ (meet F)
by A2; :: thesis: verum
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 )

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

end;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

then
not x in meet F
by Def1;
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;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

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