let L, M be non empty RelStr ; ( L,M are_isomorphic & L is antisymmetric implies M is antisymmetric )
assume that
A1:
L,M are_isomorphic
and
A2:
L is antisymmetric
; M is antisymmetric
M,L are_isomorphic
by A1, WAYBEL_1:6;
then consider f being Function of M,L such that
A3:
f is isomorphic
;
let x, y be Element of M; YELLOW_0:def 3 ( not x <= y or not y <= x or x = y )
assume A4:
( x <= y & y <= x )
; x = y
reconsider fy = f . y as Element of L ;
reconsider fx = f . x as Element of L ;
( fx <= fy & fy <= fx )
by A3, A4, WAYBEL_0:66;
then
( dom f = the carrier of M & fx = fy )
by A2, FUNCT_2:def 1;
hence
x = y
by A3, FUNCT_1:def 4; verum