let X be Subset of REAL; :: thesis: ( X is compact implies X is closed )
assume A1: X is compact ; :: thesis: X is closed
assume not X is closed ; :: thesis: contradiction
then consider s1 being Real_Sequence such that
A2: rng s1 c= X and
A3: ( s1 is convergent & not lim s1 in X ) ;
ex s2 being Real_Sequence st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) by A1, A2;
hence contradiction by A3, SEQ_4:17; :: thesis: verum