let T be non empty RelStr ; :: thesis: for N being net of T
for M being non empty full SubNetStr of N st ( for i being Element of N ex j being Element of N st
( j >= i & j in the carrier of M ) ) holds
( M is subnet of N & incl M,N is Embedding of M,N )
let N be net of T; :: thesis: for M being non empty full SubNetStr of N st ( for i being Element of N ex j being Element of N st
( j >= i & j in the carrier of M ) ) holds
( M is subnet of N & incl M,N is Embedding of M,N )
let M be non empty full SubNetStr of N; :: thesis: ( ( for i being Element of N ex j being Element of N st
( j >= i & j in the carrier of M ) ) implies ( M is subnet of N & incl M,N is Embedding of M,N ) )
assume A1: for i being Element of N ex j being Element of N st
( j >= i & j in the carrier of M ) ; :: thesis: ( M is subnet of N & incl M,N is Embedding of M,N )
A2: ( the mapping of M = the mapping of N | the carrier of M & M is full SubRelStr of N ) by YELLOW_6:def 8, YELLOW_6:def 9;
then A3: the carrier of M c= the carrier of N by YELLOW_0:def 13;
M is directed

proof

let x, y be Element of M; :: according to YELLOW_6:def 5 :: thesis: ex b₁ being Element of the carrier of M st
( x <= b₁ & y <= b₁ )
reconsider i = x, j = y as Element of N by A2, YELLOW_0:59;
consider k being Element of N such that
A4: ( k >= i & k >= j ) by YELLOW_6:def 5;
consider l being Element of N such that
A5: ( l >= k & l in the carrier of M ) by A1;
reconsider z = l as Element of M by A5;
take z ; :: thesis: ( x <= z & y <= z )
( l >= i & l >= j ) by A4, A5, YELLOW_0:def 2;
hence ( x <= z & y <= z ) by YELLOW_6:21; :: thesis: verum

end;

then reconsider K = M as net of T by A2;

A6: now

set f = incl K,N;
A7: incl K,N = id the carrier of K by A3, YELLOW_9:def 1;
hence the mapping of K = the mapping of N * (incl K,N) by A2, RELAT_1:94; :: thesis: for m being Element of N ex n being Element of K st
for p being Element of K st n <= p holds
m <= (incl K,N) . p
let m be Element of N; :: thesis: ex n being Element of K st
for p being Element of K st n <= p holds
m <= (incl K,N) . p
consider j being Element of N such that
A8: ( j >= m & j in the carrier of K ) by A1;
reconsider n = j as Element of K by A8;
take n = n; :: thesis: for p being Element of K st n <= p holds
m <= (incl K,N) . p
let p be Element of K; :: thesis: ( n <= p implies m <= (incl K,N) . p )
reconsider q = p as Element of N by A2, YELLOW_0:59;
assume n <= p ; :: thesis: m <= (incl K,N) . p
then ( j <= q & (incl K,N) . p = q ) by A7, FUNCT_1:35, YELLOW_6:20;
hence m <= (incl K,N) . p by A8, YELLOW_0:def 2; :: thesis: verum

end;

hence M is subnet of N by YELLOW_6:def 12; :: thesis: incl M,N is Embedding of M,N
hence incl M,N is Embedding of M,N by A6, Def3; :: thesis: verum