:: deftheorem defines PartialPredConnectivesLatt PARTPR_1:def 14 :
for D being non empty set holds PartialPredConnectivesLatt D = OrthoLattStr(# (Pr D),(PartialPredConnectivesJoin D),(PartialPredConnectivesMeet D),(PartialPredConnectivesCompl D) #);