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} by Lm2, PARTIT_2:19, ENUMSET1:29;
for x being Element of TrivOrthoRelStr 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 TrivOrthoRelStr; :: 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 Th14; :: thesis: verum

end;

hence TrivOrthoRelStr is QuasiOrthocomplemented ; :: thesis: verum