let L be RelStr ; :: thesis: ( L is transitive iff L opp is transitive )
thus ( L is transitive implies L opp is transitive ) :: thesis: ( L opp is transitive implies L is transitive )

proof

assume A1: L is transitive ; :: thesis: L opp is transitive
let x, y, z be Element of (L opp); :: according to YELLOW_0:def 2 :: thesis: ( not x <= y or not y <= z or x <= z )
assume ( x <= y & z >= y ) ; :: thesis: x <= z
then ( ~ x >= ~ y & ~ z <= ~ y ) by Th1;
hence x <= z by Th1, A1; :: thesis: verum

end;

assume A2: L opp is transitive ; :: thesis: L is transitive
let x, y, z be Element of L; :: according to YELLOW_0:def 2 :: thesis: ( not x <= y or not y <= z or x <= z )
assume ( x <= y & z >= y ) ; :: thesis: x <= z
then ( x ~ >= y ~ & z ~ <= y ~ ) by LATTICE3:9;
then x ~ >= z ~ by A2;
hence x <= z by LATTICE3:9; :: thesis: verum