let L, M be non empty RelStr ; :: thesis: ( L,M are_isomorphic & L is reflexive implies M is reflexive )
assume that
A1: L,M are_isomorphic and
A2: L is reflexive ; :: thesis: M is reflexive
let x be Element of M; :: according to YELLOW_0:def 1 :: thesis: x <= x
M,L are_isomorphic by A1, WAYBEL_1:6;
then consider f being Function of M,L such that
A3: f is isomorphic ;
reconsider fx = f . x as Element of L ;
fx <= fx by A2;
hence x <= x by A3, WAYBEL_0:66; :: thesis: verum