theorem PosReg: :: ROUGHS_3:24

for L1, L2 being non empty RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is positive_alliance holds
L2 is positive_alliance ;