take PartialPredConnectivesLatt the non empty set ; :: thesis: ( PartialPredConnectivesLatt the non empty set is partially_Boolean & PartialPredConnectivesLatt the non empty set is join-idempotent & PartialPredConnectivesLatt the non empty set is Lattice-like )
thus ( PartialPredConnectivesLatt the non empty set is partially_Boolean & PartialPredConnectivesLatt the non empty set is join-idempotent & PartialPredConnectivesLatt the non empty set is Lattice-like ) ; :: thesis: verum