let X, SFY be set ; X /\ (union SFY) = union (INTERSECTION ({X},SFY))
A1:
union (INTERSECTION ({X},SFY)) c= X /\ (union SFY)
proof
let x be
object ;
TARSKI:def 3 ( not x in union (INTERSECTION ({X},SFY)) or x in X /\ (union SFY) )
assume
x in union (INTERSECTION ({X},SFY))
;
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;
verum
end;
X /\ (union SFY) c= union (INTERSECTION ({X},SFY))
hence
X /\ (union SFY) = union (INTERSECTION ({X},SFY))
by A1; verum