:: deftheorem defines partially_complemented PARTPR_1:def 16 :
for L being non empty constituted-Functions LattStr holds
( L is partially_complemented iff for b being Element of L ex a being Element of L st a is_a_partial_complement_of b );