consider T being non empty compact TopSpace;
take T ; :: thesis: ( not T is empty & T is compact )
thus ( not T is empty & T is compact ) ; :: thesis: verum