let X be set ; :: thesis: for F being Subset-Family of X holds
( F is Cover of X iff union F = X )
let F be Subset-Family of X; :: thesis: ( F is Cover of X iff union F = X )
thus ( F is Cover of X implies union F = X ) :: thesis: ( union F = X implies F is Cover of X )

proof

assume A1: F is Cover of X ; :: thesis: union F = X
thus union F c= X ; :: according to XBOOLE_0:def 10 :: thesis: X c= union F
thus X c= union F by A1, Def12; :: thesis: verum

end;

thus ( union F = X implies F is Cover of X ) by Def12; :: thesis: verum