let X be set ; :: thesis: for S being non empty Subset-Family of X holds
( meet S = X \ (union (X \ S)) & union S = X \ (meet (X \ S)) )
let S be non empty Subset-Family of X; :: thesis: ( meet S = X \ (union (X \ S)) & union S = X \ (meet (X \ S)) )
A1: X \ (union (X \ S)) c= meet S
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X \ (union (X \ S)) or x in meet S )
assume A2: x in X \ (union (X \ S)) ; :: thesis: x in meet S
then A3: not x in union (X \ S) by XBOOLE_0:def 5;
for Y being set st Y in S holds
x in Y
proof
let Y be set ; :: thesis: ( Y in S implies x in Y )
assume that
A4: Y in S and
A5: not x in Y ; :: thesis: contradiction
reconsider Y = Y as Subset of X by A4;
(Y `) ` in S by A4;
then A6: Y ` in X \ S by SETFAM_1:def 7;
x in Y ` by A2, A5, SUBSET_1:29;
hence contradiction by A3, A6, TARSKI:def 4; :: thesis: verum
end;
hence x in meet S by SETFAM_1:def 1; :: thesis: verum
end;
meet S c= X \ (union (X \ S))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet S or x in X \ (union (X \ S)) )
assume A7: x in meet S ; :: thesis: x in X \ (union (X \ S))
not x in union (X \ S)
proof
assume x in union (X \ S) ; :: thesis: contradiction
then consider Z being set such that
A8: x in Z and
A9: Z in X \ S by TARSKI:def 4;
reconsider Z = Z as Subset of X by A9;
( Z ` in S & not x in Z ` ) by A8, A9, SETFAM_1:def 7, XBOOLE_0:def 5;
hence contradiction by A7, SETFAM_1:def 1; :: thesis: verum
end;
hence x in X \ (union (X \ S)) by A7, XBOOLE_0:def 5; :: thesis: verum
end;
hence meet S = X \ (union (X \ S)) by A1; :: thesis: union S = X \ (meet (X \ S))
thus union S c= X \ (meet (X \ S)) :: according to XBOOLE_0:def 10 :: thesis: X \ (meet (X \ S)) c= union S
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union S or x in X \ (meet (X \ S)) )
assume x in union S ; :: thesis: x in X \ (meet (X \ S))
then consider Y being set such that
A10: x in Y and
A11: Y in S by TARSKI:def 4;
reconsider Y = Y as Subset of X by A11;
not x in meet (X \ S)
proof
(Y `) ` in S by A11;
then A12: Y ` in X \ S by SETFAM_1:def 7;
assume A13: x in meet (X \ S) ; :: thesis: contradiction
not x in Y ` by A10, XBOOLE_0:def 5;
hence contradiction by A13, A12, SETFAM_1:def 1; :: thesis: verum
end;
hence x in X \ (meet (X \ S)) by A10, A11, XBOOLE_0:def 5; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X \ (meet (X \ S)) or x in union S )
assume A14: x in X \ (meet (X \ S)) ; :: thesis: x in union S
then not x in meet (X \ S) by XBOOLE_0:def 5;
then consider Z being set such that
A15: Z in X \ S and
A16: not x in Z by SETFAM_1:def 1;
reconsider Z = Z as Subset of X by A15;
A17: Z ` in S by A15, SETFAM_1:def 7;
x in Z ` by A14, A16, SUBSET_1:29;
hence x in union S by A17, TARSKI:def 4; :: thesis: verum