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