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

proof

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

end;

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