let D be set ; :: thesis: for F being Subset-Family of D st F <> {} holds

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

let F be Subset-Family of D; :: thesis: ( F <> {} implies ([#] D) \ (union F) = meet (COMPLEMENT F) )

A1: for x being object st x in D holds

( ( for X being set st X in F holds

not x in X ) iff for Y being set st Y in COMPLEMENT F holds

x in Y )

then A7: COMPLEMENT F <> {} by Th32;

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

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

let F be Subset-Family of D; :: thesis: ( F <> {} implies ([#] D) \ (union F) = meet (COMPLEMENT F) )

A1: for x being object st x in D holds

( ( for X being set st X in F holds

not x in X ) iff for Y being set st Y in COMPLEMENT F holds

x in Y )

proof

assume
F <> {}
; :: thesis: ([#] D) \ (union F) = meet (COMPLEMENT F)
let x be object ; :: thesis: ( x in D implies ( ( for X being set st X in F holds

not x in X ) iff for Y being set st Y in COMPLEMENT F holds

x in Y ) )

assume A2: x in D ; :: thesis: ( ( for X being set st X in F holds

not x in X ) iff for Y being set st Y in COMPLEMENT F holds

x in Y )

thus ( ( for X being set st X in F holds

not x in X ) implies for Y being set st Y in COMPLEMENT F holds

x in Y ) :: thesis: ( ( for Y being set st Y in COMPLEMENT F holds

x in Y ) implies for X being set st X in F holds

not x in X )

x in Y ; :: thesis: for X being set st X in F holds

not x in X

let X be set ; :: thesis: ( X in F implies not x in X )

assume A6: X in F ; :: thesis: not x in X

then reconsider X = X as Subset of D ;

(X `) ` = X ;

then X ` in COMPLEMENT F by A6, Def7;

then x in X ` by A5;

hence not x in X by XBOOLE_0:def 5; :: thesis: verum

end;not x in X ) iff for Y being set st Y in COMPLEMENT F holds

x in Y ) )

assume A2: x in D ; :: thesis: ( ( for X being set st X in F holds

not x in X ) iff for Y being set st Y in COMPLEMENT F holds

x in Y )

thus ( ( for X being set st X in F holds

not x in X ) implies for Y being set st Y in COMPLEMENT F holds

x in Y ) :: thesis: ( ( for Y being set st Y in COMPLEMENT F holds

x in Y ) implies for X being set st X in F holds

not x in X )

proof

assume A5:
for Y being set st Y in COMPLEMENT F holds
assume A3:
for X being set st X in F holds

not x in X ; :: thesis: for Y being set st Y in COMPLEMENT F holds

x in Y

let Y be set ; :: thesis: ( Y in COMPLEMENT F implies x in Y )

assume A4: Y in COMPLEMENT F ; :: thesis: x in Y

then reconsider Y = Y as Subset of D ;

Y ` in F by A4, Def7;

then not x in Y ` by A3;

hence x in Y by A2, XBOOLE_0:def 5; :: thesis: verum

end;not x in X ; :: thesis: for Y being set st Y in COMPLEMENT F holds

x in Y

let Y be set ; :: thesis: ( Y in COMPLEMENT F implies x in Y )

assume A4: Y in COMPLEMENT F ; :: thesis: x in Y

then reconsider Y = Y as Subset of D ;

Y ` in F by A4, Def7;

then not x in Y ` by A3;

hence x in Y by A2, XBOOLE_0:def 5; :: thesis: verum

x in Y ; :: thesis: for X being set st X in F holds

not x in X

let X be set ; :: thesis: ( X in F implies not x in X )

assume A6: X in F ; :: thesis: not x in X

then reconsider X = X as Subset of D ;

(X `) ` = X ;

then X ` in COMPLEMENT F by A6, Def7;

then x in X ` by A5;

hence not x in X by XBOOLE_0:def 5; :: thesis: verum

then A7: COMPLEMENT F <> {} by Th32;

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

proof

meet (COMPLEMENT F) c= ([#] D) \ (union F)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ([#] D) \ (union F) or x in meet (COMPLEMENT F) )

assume A9: x in ([#] D) \ (union F) ; :: thesis: x in meet (COMPLEMENT F)

then not x in union F by XBOOLE_0:def 5;

then for X being set st X in F holds

not x in X by TARSKI:def 4;

then for Y being set st Y in COMPLEMENT F holds

x in Y by A1, A9;

hence x in meet (COMPLEMENT F) by A7, Def1; :: thesis: verum

end;assume A9: x in ([#] D) \ (union F) ; :: thesis: x in meet (COMPLEMENT F)

then not x in union F by XBOOLE_0:def 5;

then for X being set st X in F holds

not x in X by TARSKI:def 4;

then for Y being set st Y in COMPLEMENT F holds

x in Y by A1, A9;

hence x in meet (COMPLEMENT F) by A7, Def1; :: thesis: verum

proof

hence
([#] D) \ (union F) = meet (COMPLEMENT F)
by A8; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet (COMPLEMENT F) or x in ([#] D) \ (union F) )

assume A10: x in meet (COMPLEMENT F) ; :: thesis: x in ([#] D) \ (union F)

then for X being set st X in COMPLEMENT F holds

x in X by Def1;

then for Y being set st x in Y holds

not Y in F by A1;

then not x in union F by TARSKI:def 4;

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

end;assume A10: x in meet (COMPLEMENT F) ; :: thesis: x in ([#] D) \ (union F)

then for X being set st X in COMPLEMENT F holds

x in X by Def1;

then for Y being set st x in Y holds

not Y in F by A1;

then not x in union F by TARSKI:def 4;

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