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 A1: g OrthoComplement_on PO ; :: thesis: g QuasiOrthoComplement_on PO
then A2: for x being Element of PO holds
( ex_sup_of {x,(g . x)},PO & ex_inf_of {x,(g . x)},PO ) by Def36;
g is Orderinvolutive by A1, Def36;
hence g QuasiOrthoComplement_on PO by A2, Def34; :: thesis: verum