let T1, T2 be TopSpace; :: thesis: for S1 being Subset of T1
for S2 being Subset of T2 st S1 is compact & S2 is compact holds
[:S1,S2:] is compact Subset of [:T1,T2:]
let S1 be Subset of T1; :: thesis: for S2 being Subset of T2 st S1 is compact & S2 is compact holds
[:S1,S2:] is compact Subset of [:T1,T2:]
let S2 be Subset of T2; :: thesis: ( S1 is compact & S2 is compact implies [:S1,S2:] is compact Subset of [:T1,T2:] )
assume A1:
( S1 is compact & S2 is compact )
; :: thesis: [:S1,S2:] is compact Subset of [:T1,T2:]
per cases
( ( not S1 is empty & not S2 is empty ) or ( S1 is empty & not S2 is empty ) or ( not S1 is empty & S2 is empty ) or ( S1 is empty & S2 is empty ) )
;
suppose A2:
( not
S1 is
empty & not
S2 is
empty )
;
:: thesis: [:S1,S2:] is compact Subset of [:T1,T2:]then consider x being
set such that A3:
x in S1
by XBOOLE_0:def 1;
consider y being
set such that A4:
y in S2
by A2, XBOOLE_0:def 1;
reconsider T1 =
T1,
T2 =
T2 as non
empty TopSpace by A3, A4;
reconsider S1 =
S1 as non
empty compact Subset of
T1 by A1, A2;
reconsider S2 =
S2 as non
empty compact Subset of
T2 by A1, A2;
reconsider X =
[:S1,S2:] as
Subset of
[:T1,T2:] ;
TopStruct(# the
carrier of
[:(T1 | S1),(T2 | S2):],the
topology of
[:(T1 | S1),(T2 | S2):] #)
= TopStruct(# the
carrier of
([:T1,T2:] | X),the
topology of
([:T1,T2:] | X) #)
by Th26;
hence
[:S1,S2:] is
compact Subset of
[:T1,T2:]
by COMPTS_1:12;
:: thesis: verum end;