let X be set ; :: thesis: for D being a_partition of X
for A, B being Subset of D holds union (A /\ B) = (union A) /\ (union B)
let D be a_partition of X; :: thesis: for A, B being Subset of D holds union (A /\ B) = (union A) /\ (union B)
let A, B be Subset of D; :: thesis: union (A /\ B) = (union A) /\ (union B)
thus union (A /\ B) c= (union A) /\ (union B) by ZFMISC_1:79; :: according to XBOOLE_0:def 10 :: thesis: (union A) /\ (union B) c= union (A /\ B)
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in (union A) /\ (union B) or e in union (A /\ B) )
assume A1: e in (union A) /\ (union B) ; :: thesis: e in union (A /\ B)
then e in union A by XBOOLE_0:def 4;
then consider a being set such that
A2: e in a and
A3: a in A by TARSKI:def 4;
A4: a in D by A3;
e in union B by A1, XBOOLE_0:def 4;
then consider b being set such that
A5: e in b and
A6: b in B by TARSKI:def 4;
A7: b in D by A6;
not a misses b by A2, A5, XBOOLE_0:3;
then a = b by A4, A7, Def4;
then a in A /\ B by A3, A6, XBOOLE_0:def 4;
hence e in union (A /\ B) by A2, TARSKI:def 4; :: thesis: verum