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 & s1 is convergent & not lim s1 in X ) by Def4;
ex s2 being Real_Sequence st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) by A1, A2, Def3;
hence contradiction by A2, SEQ_4:30; :: thesis: verum