let A, B be compact Subset of REAL ; :: thesis: A /\ B is compact
let s1 be Real_Sequence; :: according to RCOMP_1:def 3 :: thesis: ( not rng s1 c= A /\ B or ex b₁ being Element of bool [:NAT ,REAL :] st
( b₁ is subsequence of s1 & b₁ is convergent & lim b₁ in A /\ B ) )
assume A1: rng s1 c= A /\ B ; :: thesis: ex b₁ being Element of bool [:NAT ,REAL :] st
( b₁ is subsequence of s1 & b₁ is convergent & lim b₁ in A /\ B )
A /\ B c= A by XBOOLE_1:17;
then rng s1 c= A by A1, XBOOLE_1:1;
then consider s2 being Real_Sequence such that
A2: s2 is subsequence of s1 and
A3: s2 is convergent and
A4: lim s2 in A by RCOMP_1:def 3;
rng s2 c= rng s1 by A2, VALUED_0:21;
then A5: rng s2 c= A /\ B by A1, XBOOLE_1:1;
A /\ B c= B by XBOOLE_1:17;
then rng s2 c= B by A5, XBOOLE_1:1;
then consider s3 being Real_Sequence such that
A6: s3 is subsequence of s2 and
A7: s3 is convergent and
A8: lim s3 in B by RCOMP_1:def 3;
take s3 ; :: thesis: ( s3 is subsequence of s1 & s3 is convergent & lim s3 in A /\ B )
thus s3 is subsequence of s1 by A2, A6, VALUED_0:20; :: thesis: ( s3 is convergent & lim s3 in A /\ B )
thus s3 is convergent by A7; :: thesis: lim s3 in A /\ B
lim s3 = lim s2 by A3, A6, SEQ_4:30;
hence lim s3 in A /\ B by A4, A8, XBOOLE_0:def 4; :: thesis: verum