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 EQREL_1:def 6;
hence B ` c= union (A ` ) by A1, Th18; :: according to XBOOLE_0:def 10 :: thesis: union (A ` ) c= B `
let e be set ; :: 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 & u in A ` ) by TARSKI:def 4;
A3: u in D by A2;
assume not e in B ` ; :: thesis: contradiction
then e in B by A2, A3, SUBSET_1:50;
then consider v being set such that
A4: ( e in v & v in A ) by A1, TARSKI:def 4;
A5: v in D by A4;
not u misses v by A2, A4, XBOOLE_0:3;
then u = v by A3, A5, EQREL_1:def 6;
hence contradiction by A2, A4, XBOOLE_0:def 5; :: thesis: verum