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 proj2 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 )
A2: A /\ B c= B by XBOOLE_1:17;
A /\ B c= A by XBOOLE_1:17;
then rng s1 c= A by A1;
then consider s2 being Real_Sequence such that
A3: s2 is subsequence of s1 and
A4: s2 is convergent and
A5: lim s2 in A by RCOMP_1:def 3;
rng s2 c= rng s1 by A3, VALUED_0:21;
then rng s2 c= A /\ B by A1;
then rng s2 c= B by A2;
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 A3, 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 A4, A6, SEQ_4:17;
hence lim s3 in A /\ B by A5, A8, XBOOLE_0:def 4; :: thesis: verum