for PO being non empty OrthoRelStr
for f being UnOp of the carrier of PO st f OrthoComplement_on PO holds
f QuasiOrthoComplement_on PO ;