set T = the non empty compact TopSpace;
take the non empty compact TopSpace ; :: thesis: ( not the non empty compact TopSpace is empty & the non empty compact TopSpace is compact )
thus ( not the non empty compact TopSpace is empty & the non empty compact TopSpace is compact ) ; :: thesis: verum