let X, SFY be set ; :: thesis: X /\ (union SFY) = union (INTERSECTION ({X},SFY))

A1: union (INTERSECTION ({X},SFY)) c= X /\ (union SFY)

A1: union (INTERSECTION ({X},SFY)) c= X /\ (union SFY)

proof

X /\ (union SFY) c= union (INTERSECTION ({X},SFY))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (INTERSECTION ({X},SFY)) or x in X /\ (union SFY) )

assume x in union (INTERSECTION ({X},SFY)) ; :: thesis: x in X /\ (union SFY)

then consider Z being set such that

A2: x in Z and

A3: Z in INTERSECTION ({X},SFY) by TARSKI:def 4;

consider X1, X2 being set such that

A4: X1 in {X} and

A5: X2 in SFY and

A6: Z = X1 /\ X2 by A3, Def5;

x in X2 by A2, A6, XBOOLE_0:def 4;

then A7: x in union SFY by A5, TARSKI:def 4;

X1 = X by A4, TARSKI:def 1;

then x in X by A2, A6, XBOOLE_0:def 4;

hence x in X /\ (union SFY) by A7, XBOOLE_0:def 4; :: thesis: verum

end;assume x in union (INTERSECTION ({X},SFY)) ; :: thesis: x in X /\ (union SFY)

then consider Z being set such that

A2: x in Z and

A3: Z in INTERSECTION ({X},SFY) by TARSKI:def 4;

consider X1, X2 being set such that

A4: X1 in {X} and

A5: X2 in SFY and

A6: Z = X1 /\ X2 by A3, Def5;

x in X2 by A2, A6, XBOOLE_0:def 4;

then A7: x in union SFY by A5, TARSKI:def 4;

X1 = X by A4, TARSKI:def 1;

then x in X by A2, A6, XBOOLE_0:def 4;

hence x in X /\ (union SFY) by A7, XBOOLE_0:def 4; :: thesis: verum

proof

hence
X /\ (union SFY) = union (INTERSECTION ({X},SFY))
by A1; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X /\ (union SFY) or x in union (INTERSECTION ({X},SFY)) )

assume A8: x in X /\ (union SFY) ; :: thesis: x in union (INTERSECTION ({X},SFY))

then x in union SFY by XBOOLE_0:def 4;

then consider Y being set such that

A9: x in Y and

A10: Y in SFY by TARSKI:def 4;

x in X by A8, XBOOLE_0:def 4;

then A11: x in X /\ Y by A9, XBOOLE_0:def 4;

X in {X} by TARSKI:def 1;

then X /\ Y in INTERSECTION ({X},SFY) by A10, Def5;

hence x in union (INTERSECTION ({X},SFY)) by A11, TARSKI:def 4; :: thesis: verum

end;assume A8: x in X /\ (union SFY) ; :: thesis: x in union (INTERSECTION ({X},SFY))

then x in union SFY by XBOOLE_0:def 4;

then consider Y being set such that

A9: x in Y and

A10: Y in SFY by TARSKI:def 4;

x in X by A8, XBOOLE_0:def 4;

then A11: x in X /\ Y by A9, XBOOLE_0:def 4;

X in {X} by TARSKI:def 1;

then X /\ Y in INTERSECTION ({X},SFY) by A10, Def5;

hence x in union (INTERSECTION ({X},SFY)) by A11, TARSKI:def 4; :: thesis: verum