theorem Th40: :: WAYBEL21:40

for T being non empty RelStr
for N being net of T
for i being Element of N holds
( N | i is subnet of N & incl ((N | i),N) is Embedding of N | i,N )