let Z be Subset-Family of REAL; :: thesis: ( Z is closed implies meet Z is closed )
assume A1: Z is closed ; :: thesis: meet Z is closed
let seq be Real_Sequence; :: according to RCOMP_1:def 4 :: thesis: ( not rng seq c= meet Z or not seq is convergent or lim seq in meet Z )
set mZ = meet Z;
assume that
A2: rng seq c= meet Z and
A3: seq is convergent ; :: thesis: lim seq in meet Z

per cases ( Z = {} or Z <> {} ) ;

suppose Z = {} ; :: thesis: lim seq in meet Z

then meet Z = {} by SETFAM_1:def 1;
hence lim seq in meet Z by A2; :: thesis: verum

end;

suppose A4: Z <> {} ; :: thesis: lim seq in meet Z

now :: thesis: for X being set st X in Z holds
lim seq in X

let X be set ; :: thesis: ( X in Z implies lim seq in X )
assume A5: X in Z ; :: thesis: lim seq in X
then reconsider X9 = X as Subset of REAL ;
A6: rng seq c= X by A2, A5, SETFAM_1:def 1;
X9 is closed by A1, A5;
hence lim seq in X by A3, A6; :: thesis: verum

end;

hence lim seq in meet Z by A4, SETFAM_1:def 1; :: thesis: verum

end;

end;