let X be set ; :: thesis: for B being Subset-Family of X holds

( B is covering iff for x being set st x in X holds

ex U being Subset of X st

( U in B & x in U ) )

let B be Subset-Family of X; :: thesis: ( B is covering iff for x being set st x in X holds

ex U being Subset of X st

( U in B & x in U ) )

ex U being Subset of X st

( U in B & x in U ) ; :: thesis: B is covering

union B = X

( B is covering iff for x being set st x in X holds

ex U being Subset of X st

( U in B & x in U ) )

let B be Subset-Family of X; :: thesis: ( B is covering iff for x being set st x in X holds

ex U being Subset of X st

( U in B & x in U ) )

hereby :: thesis: ( ( for x being set st x in X holds

ex U being Subset of X st

( U in B & x in U ) ) implies B is covering )

assume A4:
for x being set st x in X holds ex U being Subset of X st

( U in B & x in U ) ) implies B is covering )

assume
B is covering
; :: thesis: for x being set st x in X holds

ex U being Subset of X st

( U in B & x in U )

then A1: union B = X by ABIAN:4;

let x be set ; :: thesis: ( x in X implies ex U being Subset of X st

( U in B & x in U ) )

assume x in X ; :: thesis: ex U being Subset of X st

( U in B & x in U )

then consider U being set such that

A2: x in U and

A3: U in B by A1, TARSKI:def 4;

reconsider U = U as Subset of X by A3;

take U = U; :: thesis: ( U in B & x in U )

thus ( U in B & x in U ) by A2, A3; :: thesis: verum

end;ex U being Subset of X st

( U in B & x in U )

then A1: union B = X by ABIAN:4;

let x be set ; :: thesis: ( x in X implies ex U being Subset of X st

( U in B & x in U ) )

assume x in X ; :: thesis: ex U being Subset of X st

( U in B & x in U )

then consider U being set such that

A2: x in U and

A3: U in B by A1, TARSKI:def 4;

reconsider U = U as Subset of X by A3;

take U = U; :: thesis: ( U in B & x in U )

thus ( U in B & x in U ) by A2, A3; :: thesis: verum

ex U being Subset of X st

( U in B & x in U ) ; :: thesis: B is covering

union B = X

proof

hence
B is covering
by ABIAN:4; :: thesis: verum
thus
union B c= X
; :: according to XBOOLE_0:def 10 :: thesis: X c= union B

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in X or a in union B )

assume a in X ; :: thesis: a in union B

then ex U being Subset of X st

( U in B & a in U ) by A4;

hence a in union B by TARSKI:def 4; :: thesis: verum

end;let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in X or a in union B )

assume a in X ; :: thesis: a in union B

then ex U being Subset of X st

( U in B & a in U ) by A4;

hence a in union B by TARSKI:def 4; :: thesis: verum