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