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

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