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

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