set O = TrivOrthoRelStr ;
set C = the Compl of TrivOrthoRelStr ;
reconsider Emp = {} as Element of TrivOrthoRelStr by CARD_1:87, 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 CARD_1:87, FUNCT_2:65;
then f . a2 <= f . a1 by CARD_1:87, FUNCT_2:65;
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 by Def32, Th19; :: thesis: verum