theorem Th3: :: WAYBEL33:3

for L1, L2 being non empty 1-sorted st the carrier of L1 = the carrier of L2 holds
for N1 being NetStr over L1 st N1 in NetUniv L1 holds
ex N2 being strict net of L2 st
( N2 in NetUniv L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 )