set O = TrivOrthoRelStr ;
set C = the Compl of TrivOrthoRelStr;
reconsider Emp = {} as Element of TrivOrthoRelStr by TARSKI:def 1;
the Compl of TrivOrthoRelStr is antitone Function of TrivOrthoRelStr,TrivOrthoRelStr

proof

reconsider f = the Compl of TrivOrthoRelStr as Function of TrivOrthoRelStr,TrivOrthoRelStr ;
for x1, x2 being Element of TrivOrthoRelStr st x1 <= x2 holds
for y1, y2 being Element of TrivOrthoRelStr st y1 = f . x1 & y2 = f . x2 holds
y1 >= y2

proof

let a1, a2 be Element of TrivOrthoRelStr; :: thesis: ( a1 <= a2 implies for y1, y2 being Element of TrivOrthoRelStr st y1 = f . a1 & y2 = f . a2 holds
y1 >= y2 )
set b1 = f . a1;
f . a1 = Emp by FUNCT_2:50;
then f . a2 <= f . a1 by FUNCT_2:50;
hence ( a1 <= a2 implies for y1, y2 being Element of TrivOrthoRelStr st y1 = f . a1 & y2 = f . a2 holds
y1 >= y2 ) ; :: thesis: verum

end;

hence the Compl of TrivOrthoRelStr is antitone Function of TrivOrthoRelStr,TrivOrthoRelStr by WAYBEL_0:def 5; :: thesis: verum

end;

hence the Compl of TrivOrthoRelStr is Orderinvolutive ; :: thesis: verum