let X be non empty set ; :: thesis: for D being a_partition of X

for A being Subset of D

for B being Subset of X st B = union A holds

B ` = union (A `)

let D be a_partition of X; :: thesis: for A being Subset of D

for B being Subset of X st B = union A holds

B ` = union (A `)

let A be Subset of D; :: thesis: for B being Subset of X st B = union A holds

B ` = union (A `)

let B be Subset of X; :: thesis: ( B = union A implies B ` = union (A `) )

assume A1: B = union A ; :: thesis: B ` = union (A `)

union D = X by Def4;

hence B ` c= union (A `) by A1, Th55; :: according to XBOOLE_0:def 10 :: thesis: union (A `) c= B `

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in union (A `) or e in B ` )

assume e in union (A `) ; :: thesis: e in B `

then consider u being set such that

A2: e in u and

A3: u in A ` by TARSKI:def 4;

A4: u in D by A3;

assume not e in B ` ; :: thesis: contradiction

then e in B by A2, A4, SUBSET_1:29;

then consider v being set such that

A5: e in v and

A6: v in A by A1, TARSKI:def 4;

A7: v in D by A6;

not u misses v by A2, A5, XBOOLE_0:3;

then u = v by A4, A7, Def4;

hence contradiction by A3, A6, XBOOLE_0:def 5; :: thesis: verum

for A being Subset of D

for B being Subset of X st B = union A holds

B ` = union (A `)

let D be a_partition of X; :: thesis: for A being Subset of D

for B being Subset of X st B = union A holds

B ` = union (A `)

let A be Subset of D; :: thesis: for B being Subset of X st B = union A holds

B ` = union (A `)

let B be Subset of X; :: thesis: ( B = union A implies B ` = union (A `) )

assume A1: B = union A ; :: thesis: B ` = union (A `)

union D = X by Def4;

hence B ` c= union (A `) by A1, Th55; :: according to XBOOLE_0:def 10 :: thesis: union (A `) c= B `

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in union (A `) or e in B ` )

assume e in union (A `) ; :: thesis: e in B `

then consider u being set such that

A2: e in u and

A3: u in A ` by TARSKI:def 4;

A4: u in D by A3;

assume not e in B ` ; :: thesis: contradiction

then e in B by A2, A4, SUBSET_1:29;

then consider v being set such that

A5: e in v and

A6: v in A by A1, TARSKI:def 4;

A7: v in D by A6;

not u misses v by A2, A5, XBOOLE_0:3;

then u = v by A4, A7, Def4;

hence contradiction by A3, A6, XBOOLE_0:def 5; :: thesis: verum