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