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 A1: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & the InternalRel of L1 is_reflexive_in the carrier of L1 ) ; :: according to ORDERS_2:def 2 :: thesis: L2 is reflexive
let x be set ; :: according to RELAT_2:def 1,ORDERS_2:def 2 :: 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, RELAT_2:def 1; :: thesis: verum