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 by YELLOW_6:def 6;
A3: M is full SubRelStr of N by YELLOW_6:def 7;
then A4: 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 3 :: 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 A3, YELLOW_0:58;
consider k being Element of N such that
A5: k >= i and
A6: k >= j by YELLOW_6:def 3;
consider l being Element of N such that
A7: l >= k and
A8: l in the carrier of M by A1;
reconsider z = l as Element of M by A8;
take z ; :: thesis: ( x <= z & y <= z )
A9: l >= i by A5, A7, YELLOW_0:def 2;
l >= j by A6, A7, YELLOW_0:def 2;
hence ( x <= z & y <= z ) by A9, YELLOW_6:12; :: thesis: verum

end;

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

A10: now :: thesis: ( the mapping of K = the mapping of N * (incl (K,N)) & ( 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 ) )

set f = incl (K,N);
A11: incl (K,N) = id the carrier of K by A4, YELLOW_9:def 1;
hence the mapping of K = the mapping of N * (incl (K,N)) by A2, RELAT_1:65; :: 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
A12: j >= m and
A13: j in the carrier of K by A1;
reconsider n = j as Element of K by A13;
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 A3, YELLOW_0:58;
assume n <= p ; :: thesis: m <= (incl (K,N)) . p
then A14: j <= q by YELLOW_6:11;
(incl (K,N)) . p = q by A11;
hence m <= (incl (K,N)) . p by A12, A14, YELLOW_0:def 2; :: thesis: verum

end;

hence M is subnet of N by YELLOW_6:def 9; :: thesis: incl (M,N) is Embedding of M,N
hence incl (M,N) is Embedding of M,N by A10, Def3; :: thesis: verum