let L be non empty RelStr ; :: thesis: ( L is connected iff L opp is connected )
thus ( L is connected implies L opp is connected ) :: thesis: ( L opp is connected implies L is connected )

proof

assume A1: for x, y being Element of L holds
( x <= y or x >= y ) ; :: according to WAYBEL_0:def 29 :: thesis: L opp is connected
let x, y be Element of (L opp); :: according to WAYBEL_0:def 29 :: thesis: ( x <= y or y <= x )
( ~ x <= ~ y or ~ x >= ~ y ) by A1;
hence ( x <= y or y <= x ) by Th1; :: thesis: verum

end;

assume A2: for x, y being Element of (L opp) holds
( x <= y or x >= y ) ; :: according to WAYBEL_0:def 29 :: thesis: L is connected
let x, y be Element of L; :: according to WAYBEL_0:def 29 :: thesis: ( x <= y or y <= x )
( x ~ <= y ~ or x ~ >= y ~ ) by A2;
hence ( x <= y or y <= x ) by LATTICE3:9; :: thesis: verum