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

proof

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;

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

proof

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;

hence X /\ (union SFY) = union (INTERSECTION ({X},SFY)) by A1; :: thesis: verum