let T1, T2 be TopSpace; :: thesis: for S1 being Subset of
for S2 being Subset of st S1 is compact & S2 is compact holds
[:S1,S2:] is compact Subset of
let S1 be Subset of ; :: thesis: for S2 being Subset of st S1 is compact & S2 is compact holds
[:S1,S2:] is compact Subset of
let S2 be Subset of ; :: thesis: ( S1 is compact & S2 is compact implies [:S1,S2:] is compact Subset of )
assume that
A1: S1 is compact and
A2: S2 is compact ; :: thesis: [:S1,S2:] is compact Subset of

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 ) ; :: thesis: [:S1,S2:] is compact Subset of

then ( ex x being set st x in S1 & ex y being set st y in S2 ) by XBOOLE_0:def 1;
then reconsider T1 = T1, T2 = T2 as non empty TopSpace ;
reconsider S2 = S2 as non empty compact Subset of by A2, A3;
reconsider S1 = S1 as non empty compact Subset of by A1, A3;
reconsider X = [:S1,S2:] as Subset of ;
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 by COMPTS_1:12; :: thesis: verum

end;

suppose ( S1 is empty & not S2 is empty ) ; :: thesis: [:S1,S2:] is compact Subset of

then reconsider S1 = S1 as empty Subset of ;
[:S1,S2:] = {} [:T1,T2:] ;
hence [:S1,S2:] is compact Subset of ; :: thesis: verum

end;

suppose ( not S1 is empty & S2 is empty ) ; :: thesis: [:S1,S2:] is compact Subset of

then reconsider S2 = S2 as empty Subset of ;
[:S1,S2:] = {} [:T1,T2:] ;
hence [:S1,S2:] is compact Subset of ; :: thesis: verum

end;

suppose ( S1 is empty & S2 is empty ) ; :: thesis: [:S1,S2:] is compact Subset of

then reconsider S2 = S2 as empty Subset of ;
[:S1,S2:] = {} [:T1,T2:] ;
hence [:S1,S2:] is compact Subset of ; :: thesis: verum

end;

end;