take { the Element of T} ; :: thesis: ( not { the Element of T} is empty & { the Element of T} is compact & { the Element of T} is connected )
thus ( not { the Element of T} is empty & { the Element of T} is compact & { the Element of T} is connected ) ; :: thesis: verum