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_{1} being Element of bool [:NAT,REAL:] st

( b_{1} is subsequence of s1 & b_{1} is convergent & lim b_{1} in A /\ B ) )

assume A1: rng s1 c= A /\ B ; :: thesis: ex b_{1} being Element of bool [:NAT,REAL:] st

( b_{1} is subsequence of s1 & b_{1} is convergent & lim b_{1} 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

let s1 be Real_Sequence; :: according to RCOMP_1:def 3 :: thesis: ( not proj2 s1 c= A /\ B or ex b

( b

assume A1: rng s1 c= A /\ B ; :: thesis: ex b

( 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