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:6;
then consider f being Function of M,L such that
A3: f is isomorphic ;
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 A4: ( x <= y & y <= x ) ; :: thesis: 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; :: thesis: verum