per cases ( ( not T1 is empty & not T2 is empty ) or ( T1 is empty & T2 is empty ) or ( T1 is empty & not T2 is empty ) or ( not T1 is empty & T2 is empty ) ) ;

suppose ( not T1 is empty & not T2 is empty ) ; :: thesis: [:T1,T2:] is compact

hence [:T1,T2:] is compact by Lm5; :: thesis: verum

end;

suppose ( T1 is empty & T2 is empty ) ; :: thesis: [:T1,T2:] is compact

hence [:T1,T2:] is compact ; :: thesis: verum

end;

suppose ( T1 is empty & not T2 is empty ) ; :: thesis: [:T1,T2:] is compact

hence [:T1,T2:] is compact ; :: thesis: verum

end;

suppose ( not T1 is empty & T2 is empty ) ; :: thesis: [:T1,T2:] is compact

hence [:T1,T2:] is compact ; :: thesis: verum

end;

end;