:: deftheorem defines QuasiOrthoComplement_on OPOSET_1:def 19 :
for PO being non empty RelStr
for f being UnOp of the carrier of PO holds
( f QuasiOrthoComplement_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 ) ) ) );