let T1, T2 be TopSpace; 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; 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; ( S1 is compact & S2 is compact implies [:S1,S2:] is compact Subset of [:T1,T2:] )
assume that
A1:
S1 is compact
and
A2:
S2 is compact
; [: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 A3:
( not
S1 is
empty & not
S2 is
empty )
;
[:S1,S2:] is compact Subset of [:T1,T2:]then
( ex
x being
object st
x in S1 & ex
y being
object st
y in S2 )
;
then reconsider T1 =
T1,
T2 =
T2 as non
empty TopSpace ;
reconsider S2 =
S2 as non
empty compact Subset of
T2 by A2, A3;
reconsider S1 =
S1 as non
empty compact Subset of
T1 by A1, A3;
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 Th22;
hence
[:S1,S2:] is
compact Subset of
[:T1,T2:]
by COMPTS_1:3;
verum end; end;