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)

X \ (meet SFY) c= union (DIFFERENCE ({X},SFY))

A1: X in {X} by TARSKI:def 1;

A2: union (DIFFERENCE ({X},SFY)) c= X \ (meet SFY)

proof

assume A9:
SFY <> {}
; :: thesis: X \ (meet SFY) = union (DIFFERENCE ({X},SFY))
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 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

X \ (meet SFY) c= union (DIFFERENCE ({X},SFY))

proof

hence
X \ (meet SFY) = union (DIFFERENCE ({X},SFY))
by A2; :: thesis: verum
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;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