let X be set ; :: thesis: for D being Subset-Family of X st union D = X holds
for A being Subset of D
for B being Subset of X st B = union A holds
B ` c= union (A `)
let D be Subset-Family of X; :: thesis: ( union D = X implies for A being Subset of D
for B being Subset of X st B = union A holds
B ` c= union (A `) )
assume A1: union D = X ; :: thesis: for A being Subset of D
for B being Subset of X st B = union A holds
B ` c= union (A `)
let A be Subset of D; :: thesis: for B being Subset of X st B = union A holds
B ` c= union (A `)
let B be Subset of X; :: thesis: ( B = union A implies B ` c= union (A `) )
assume A2: B = union A ; :: thesis: B ` c= union (A `)
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in B ` or e in union (A `) )
assume A3: e in B ` ; :: thesis: e in union (A `)
then consider u being set such that
A4: e in u and
A5: u in D by A1, TARSKI:def 4;
not e in B by A3, XBOOLE_0:def 5;
then not u in A by A2, A4, TARSKI:def 4;
then u in A ` by A5, SUBSET_1:29;
hence e in union (A `) by A4, TARSKI:def 4; :: thesis: verum