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 ) )

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 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;

assume A4: for x being set st x in X holds
ex U being Subset of X st
( U in B & x in U ) ; :: thesis: B is covering
union B = X

proof

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;

hence B is covering by ABIAN:4; :: thesis: verum