let X, SFY be set ; :: thesis: ( SFY <> {} implies X \ (union SFY) = meet (DIFFERENCE ({X},SFY)) )
set y = the Element of SFY;
A1: X in {X} by TARSKI:def 1;
assume SFY <> {} ; :: thesis: X \ (union SFY) = meet (DIFFERENCE ({X},SFY))
then A2: X \ the Element of SFY in DIFFERENCE ({X},SFY) by ;
A3: meet (DIFFERENCE ({X},SFY)) c= X \ (union SFY)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet (DIFFERENCE ({X},SFY)) or x in X \ (union SFY) )
assume A4: x in meet (DIFFERENCE ({X},SFY)) ; :: thesis: x in X \ (union SFY)
for Z being set st Z in SFY holds
not x in Z
proof
let Z be set ; :: thesis: ( Z in SFY implies not x in Z )
assume Z in SFY ; :: thesis: not x in Z
then X \ Z in DIFFERENCE ({X},SFY) by ;
then x in X \ Z by ;
hence not x in Z by XBOOLE_0:def 5; :: thesis: verum
end;
then for Z being set st x in Z holds
not Z in SFY ;
then A5: not x in union SFY by TARSKI:def 4;
x in X \ the Element of SFY by A2, A4, Def1;
hence x in X \ (union SFY) by ; :: thesis: verum
end;
X \ (union SFY) c= meet (DIFFERENCE ({X},SFY))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X \ (union SFY) or x in meet (DIFFERENCE ({X},SFY)) )
assume x in X \ (union SFY) ; :: thesis: x in meet (DIFFERENCE ({X},SFY))
then A6: ( x in X & not x in union SFY ) by XBOOLE_0:def 5;
for Z being set st Z in DIFFERENCE ({X},SFY) holds
x in Z
proof
let Z be set ; :: thesis: ( Z in DIFFERENCE ({X},SFY) implies x in Z )
assume Z in DIFFERENCE ({X},SFY) ; :: thesis: x in Z
then consider Z1, Z2 being set such that
A7: ( Z1 in {X} & Z2 in SFY ) and
A8: Z = Z1 \ Z2 by Def6;
( x in Z1 & not x in Z2 ) by ;
hence x in Z by ; :: thesis: verum
end;
hence x in meet (DIFFERENCE ({X},SFY)) by ; :: thesis: verum
end;
hence X \ (union SFY) = meet (DIFFERENCE ({X},SFY)) by A3; :: thesis: verum