let T be non empty RelStr ; :: thesis:
let N be net of T; :: thesis:
let M be non empty full SubNetStr of N; :: thesis:
assume A1: for i being Element of N ex j being Element of N st
( j >= i & j in the carrier of M ) ; :: thesis:
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:
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:
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:

end;

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

A10: now :: thesis:

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:
let m be Element of N; :: thesis:
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:
let p be Element of K; :: thesis:
reconsider q = p as Element of N by A3, YELLOW_0:58;
assume n <= p ; :: thesis:
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:

end;

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