per cases ( not P is empty or P is empty ) ;

suppose not P is empty ; :: thesis: T | P is compact

hence T | P is compact by COMPTS_1:3; :: thesis: verum

end;

suppose P is empty ; :: thesis: T | P is compact

hence T | P is compact ; :: thesis: verum

end;

end;