set H = OrdRel O;

now :: thesis: for x, y being object st x in the carrier of R & y in the carrier of R & not [x,y] in OrdRel O holds
[y,x] in OrdRel O

let x, y be object ; :: thesis: ( x in the carrier of R & y in the carrier of R & not [b₁,b₂] in OrdRel O implies [b₂,b₁] in OrdRel O )
assume ( x in the carrier of R & y in the carrier of R ) ; :: thesis: ( [b₁,b₂] in OrdRel O or [b₂,b₁] in OrdRel O )
then reconsider a = x, b = y as Element of R ;
A: O \/ (- O) = the carrier of R by defpc;

per cases ( a - b in O or a - b in - O ) by A, XBOOLE_0:def 3;

suppose a - b in O ; :: thesis: ( [b₁,b₂] in OrdRel O or [b₂,b₁] in OrdRel O )

then b <= O,a ;
hence ( [x,y] in OrdRel O or [y,x] in OrdRel O ) ; :: thesis: verum

end;

suppose a - b in - O ; :: thesis: ( [b₁,b₂] in OrdRel O or [b₂,b₁] in OrdRel O )

then - (a - b) in - (- O) ;
then a <= O,b by RLVECT_1:33;
hence ( [x,y] in OrdRel O or [y,x] in OrdRel O ) ; :: thesis: verum

end;

end;

end;

hence OrdRel O is totally_connected by RELAT_2:def 7; :: thesis: verum