:: deftheorem defines is_a_partial_complement_of PARTPR_1:def 15 :
for L being non empty constituted-Functions LattStr
for a, b being Element of L holds
( a is_a_partial_complement_of b iff ( a "\/" b = (Top L) | (dom b) & b "\/" a = (Top L) | (dom b) & a "/\" b = (Bottom L) | (dom b) & b "/\" a = (Bottom L) | (dom b) ) );