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