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