let X, SFY be set ; :: thesis: ( SFY <> {} implies X \ (meet SFY) = union (DIFFERENCE ({X},SFY)) )
A1: X in {X} by TARSKI:def 1;
A2: union (DIFFERENCE ({X},SFY)) c= X \ (meet SFY)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (DIFFERENCE ({X},SFY)) or x in X \ (meet SFY) )
assume x in union (DIFFERENCE ({X},SFY)) ; :: thesis: x in X \ (meet SFY)
then consider Z being set such that
A3: x in Z and
A4: Z in DIFFERENCE ({X},SFY) by TARSKI:def 4;
consider Z1, Z2 being set such that
A5: Z1 in {X} and
A6: Z2 in SFY and
A7: Z = Z1 \ Z2 by ;
not x in Z2 by ;
then A8: not x in meet SFY by ;
Z1 = X by ;
hence x in X \ (meet SFY) by ; :: thesis: verum
end;
assume A9: SFY <> {} ; :: thesis: X \ (meet SFY) = union (DIFFERENCE ({X},SFY))
X \ (meet SFY) c= union (DIFFERENCE ({X},SFY))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X \ (meet SFY) or x in union (DIFFERENCE ({X},SFY)) )
assume A10: x in X \ (meet SFY) ; :: thesis: x in union (DIFFERENCE ({X},SFY))
then not x in meet SFY by XBOOLE_0:def 5;
then consider Z being set such that
A11: Z in SFY and
A12: not x in Z by ;
A13: x in X \ Z by ;
X \ Z in DIFFERENCE ({X},SFY) by ;
hence x in union (DIFFERENCE ({X},SFY)) by ; :: thesis: verum
end;
hence X \ (meet SFY) = union (DIFFERENCE ({X},SFY)) by A2; :: thesis: verum