let PO be non empty OrthoRelStr ; :: thesis: for f being UnOp of the carrier of PO st f OrthoComplement_on PO holds
f QuasiOrthoComplement_on PO
let g be UnOp of the carrier of PO; :: thesis: ( g OrthoComplement_on PO implies g QuasiOrthoComplement_on PO )
assume g OrthoComplement_on PO ; :: thesis: g QuasiOrthoComplement_on PO
then ( ( for x being Element of PO holds
( ex_sup_of {x,(g . x)},PO & ex_inf_of {x,(g . x)},PO ) ) & g is Orderinvolutive ) by Def36;
hence g QuasiOrthoComplement_on PO by Def34; :: thesis: verum