take PartialPredConnectivesLatt the non empty set ; :: thesis: ( not PartialPredConnectivesLatt the non empty set is empty & PartialPredConnectivesLatt the non empty set is constituted-Functions )
thus ( not PartialPredConnectivesLatt the non empty set is empty & PartialPredConnectivesLatt the non empty set is constituted-Functions ) ; :: thesis: verum