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 serial implies L2 is serial )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; :: thesis: ( not L1 is serial or L2 is serial )
assume L1 is serial ; :: thesis: L2 is serial
then the InternalRel of L1 is_serial_in the carrier of L1 by ROUGHS_2:def 3;
hence L2 is serial by A1, ROUGHS_2:def 3; :: thesis: verum