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 )

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

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

proof

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

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