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 )

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

thus ( L is transitive implies L opp is transitive ) :: thesis: ( L opp is transitive implies L is transitive )

proof

assume A2:
L opp is transitive
; :: thesis: L is transitive
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;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

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