set O = TrivOrthoRelStr ;
set C = the Compl of TrivOrthoRelStr ;
set S = the carrier of TrivOrthoRelStr ;
the Compl of TrivOrthoRelStr QuasiOrthoComplement_on TrivOrthoRelStr

proof

reconsider f = the Compl of TrivOrthoRelStr as Function of TrivOrthoRelStr ,TrivOrthoRelStr ;
A1: for x being Element of the carrier of TrivOrthoRelStr holds {x,(op1 . x)} = {x}

proof

let a be Element of the carrier of TrivOrthoRelStr ; :: thesis: {a,(op1 . a)} = {a}
a = op1 . a by Lm1, Th3, CARD_1:87, FUNCT_1:34;
hence {a,(op1 . a)} = {a} by ENUMSET1:69; :: thesis: verum

end;

for x being Element of holds
( sup {x,(f . x)} = x & inf {x,(f . x)} = x & ex_sup_of {x,(f . x)}, TrivOrthoRelStr & ex_inf_of {x,(f . x)}, TrivOrthoRelStr )

proof

let a be Element of ; :: thesis: ( sup {a,(f . a)} = a & inf {a,(f . a)} = a & ex_sup_of {a,(f . a)}, TrivOrthoRelStr & ex_inf_of {a,(f . a)}, TrivOrthoRelStr )
{a,(f . a)} = {a} by A1;
hence ( sup {a,(f . a)} = a & inf {a,(f . a)} = a & ex_sup_of {a,(f . a)}, TrivOrthoRelStr & ex_inf_of {a,(f . a)}, TrivOrthoRelStr ) by YELLOW_0:38, YELLOW_0:39; :: thesis: verum

end;

hence the Compl of TrivOrthoRelStr QuasiOrthoComplement_on TrivOrthoRelStr by Def34, Th51; :: thesis: verum

end;

hence TrivOrthoRelStr is QuasiOrthocomplemented by Def35; :: thesis: verum