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 ;
x in X2 by ;
then A7: x in union SFY by ;
X1 = X by ;
then x in X by ;
hence x in X /\ (union SFY) by ; :: 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 ;
then A11: x in X /\ Y by ;
X in {X} by TARSKI:def 1;
then X /\ Y in INTERSECTION ({X},SFY) by ;
hence x in union (INTERSECTION ({X},SFY)) by ; :: thesis: verum
end;
hence X /\ (union SFY) = union (INTERSECTION ({X},SFY)) by A1; :: thesis: verum