set O = TrivOrthoRelStr ;
set C = the Compl of TrivOrthoRelStr;
set S = the carrier of TrivOrthoRelStr;
reconsider f = the Compl of TrivOrthoRelStr as Function of TrivOrthoRelStr,TrivOrthoRelStr ;
f OrthoComplement_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;
A2: for x being Element of TrivOrthoRelStr holds
( ex_sup_of {x,(f . x)}, TrivOrthoRelStr & ex_inf_of {x,(f . x)}, TrivOrthoRelStr & sup {x,(f . x)} = x & inf {x,(f . x)} = x )

proof

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

end;

A3: for x being Element of TrivOrthoRelStr holds
( sup {x,(f . x)} in {x,(f . x)} & inf {x,(f . x)} in {x,(f . x)} )

proof

let a be Element of TrivOrthoRelStr; :: thesis: ( sup {a,(f . a)} in {a,(f . a)} & inf {a,(f . a)} in {a,(f . a)} )
( sup {a,(f . a)} = a & inf {a,(f . a)} = a ) by A2;
hence ( sup {a,(f . a)} in {a,(f . a)} & inf {a,(f . a)} in {a,(f . a)} ) by TARSKI:def 2; :: thesis: verum

end;

A4: for x being Element of TrivOrthoRelStr holds
( x is_maximum_of {x,(f . x)} & x is_minimum_of {x,(f . x)} )

proof

let a be Element of TrivOrthoRelStr; :: thesis: ( a is_maximum_of {a,(f . a)} & a is_minimum_of {a,(f . a)} )
A5: ( sup {a,(f . a)} = a & ex_sup_of {a,(f . a)}, TrivOrthoRelStr ) by A2;
( sup {a,(f . a)} in {a,(f . a)} & inf {a,(f . a)} = a ) by A2, A3;
hence ( a is_maximum_of {a,(f . a)} & a is_minimum_of {a,(f . a)} ) by A5, A2, WAYBEL_1:def 6, WAYBEL_1:def 7; :: thesis: verum

end;

for y being Element of TrivOrthoRelStr holds
( sup {y,(f . y)} is_maximum_of the carrier of TrivOrthoRelStr & inf {y,(f . y)} is_minimum_of the carrier of TrivOrthoRelStr )

proof

let a be Element of TrivOrthoRelStr; :: thesis: ( sup {a,(f . a)} is_maximum_of the carrier of TrivOrthoRelStr & inf {a,(f . a)} is_minimum_of the carrier of TrivOrthoRelStr )
reconsider a0 = a as Element of the carrier of TrivOrthoRelStr ;
{a0,(f . a0)} = {a0} by A1;
then A6: {a0,(f . a0)} = the carrier of TrivOrthoRelStr by TARSKI:def 1;
( a is_maximum_of {a,(f . a)} & a is_minimum_of {a,(f . a)} ) by A4;
hence ( sup {a,(f . a)} is_maximum_of the carrier of TrivOrthoRelStr & inf {a,(f . a)} is_minimum_of the carrier of TrivOrthoRelStr ) by A2, A6; :: thesis: verum

end;

hence f OrthoComplement_on TrivOrthoRelStr by A2, Th14; :: thesis: verum

end;

hence TrivOrthoRelStr is Orthocomplemented ; :: thesis: verum