consider A being non empty finite Subset of T;
take A ; :: thesis: ( not A is empty & A is compact )
thus ( not A is empty & A is compact ) ; :: thesis: verum