theorem Th12: :: WAYBEL28:12

for L being non empty 1-sorted
for N being net of L
for p being greater_or_equal_to_id Function of N,N holds N * p is subnet of N