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

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