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 A4, Def6;
not x in Z2 by A3, A7, XBOOLE_0:def 5;
then A8: not x in meet SFY by A6, Def1;
Z1 = X by A5, TARSKI:def 1;
hence x in X \ (meet SFY) by A3, A7, A8, XBOOLE_0:def 5; :: 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 A9, Def1;
A13: x in X \ Z by A10, A12, XBOOLE_0:def 5;
X \ Z in DIFFERENCE ({X},SFY) by A1, A11, Def6;
hence x in union (DIFFERENCE ({X},SFY)) by A13, TARSKI:def 4; :: thesis: verum

end;

hence X \ (meet SFY) = union (DIFFERENCE ({X},SFY)) by A2; :: thesis: verum