set A = the non empty finite Subset of T;
take the non empty finite Subset of T ; :: thesis: ( not the non empty finite Subset of T is empty & the non empty finite Subset of T is compact )
thus ( not the non empty finite Subset of T is empty & the non empty finite Subset of T is compact ) ; :: thesis: verum