theorem Th16: :: WAYBEL28:16

for L being non empty RelStr
for N being constant net of L
for M being subnet of N holds
( M is constant & the_value_of N = the_value_of M )