let L1, L2 be RelStr ; :: thesis: ( RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & L1 is reflexive implies L2 is reflexive )
assume that
A1: RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) and
A2: the InternalRel of L1 is_reflexive_in the carrier of L1 ; :: according to ORDERS_2:def 4 :: thesis: L2 is reflexive
let x be set ; :: according to RELAT_2:def 1,ORDERS_2:def 4 :: thesis: ( not x in the carrier of L2 or [x,x] in the InternalRel of L2 )
assume x in the carrier of L2 ; :: thesis: [x,x] in the InternalRel of L2
hence [x,x] in the InternalRel of L2 by A1, A2, RELAT_2:def 1; :: thesis: verum