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