:: deftheorem defines OrthoComplement_on OPOSET_1:def 21 :
for PO being non empty RelStr
for f being UnOp of the carrier of PO holds
( f OrthoComplement_on PO iff ( f is Orderinvolutive & ( for y being Element of PO holds
( ex_sup_of {y,(f . y)},PO & ex_inf_of {y,(f . y)},PO & "\/" ({y,(f . y)},PO) is_maximum_of the carrier of PO & "/\" ({y,(f . y)},PO) is_minimum_of the carrier of PO ) ) ) );