:: deftheorem defines QuasiOrthocomplemented OPOSET_1:def 20 :
for PO being non empty OrthoRelStr holds
( PO is QuasiOrthocomplemented iff ex f being Function of PO,PO st
( f = the Compl of PO & f QuasiOrthoComplement_on PO ) );