let T be non empty RelStr ; :: thesis: 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 )
let N be net of T; :: thesis: for i being Element of N holds
( N | i is subnet of N & incl ((N | i),N) is Embedding of N | i,N )
let i be Element of N; :: thesis: ( N | i is subnet of N & incl ((N | i),N) is Embedding of N | i,N )
set M = N | i;
set f = incl ((N | i),N);
thus N | i is subnet of N ; :: thesis: incl ((N | i),N) is Embedding of N | i,N
thus N | i is subnet of N ; :: according to WAYBEL21:def 3 :: thesis: ( the mapping of (N | i) = the mapping of N * (incl ((N | i),N)) & ( for m being Element of N ex n being Element of (N | i) st
for p being Element of (N | i) st n <= p holds
m <= (incl ((N | i),N)) . p ) )
N | i is full SubNetStr of N by WAYBEL_9:14;
then A1: N | i is full SubRelStr of N by YELLOW_6:def 7;
A2: incl ((N | i),N) = id the carrier of (N | i) by WAYBEL_9:13, YELLOW_9:def 1;
the mapping of (N | i) = the mapping of N | the carrier of (N | i) by WAYBEL_9:def 7;
hence the mapping of (N | i) = the mapping of N * (incl ((N | i),N)) by A2, RELAT_1:65; :: thesis: for m being Element of N ex n being Element of (N | i) st
for p being Element of (N | i) st n <= p holds
m <= (incl ((N | i),N)) . p
let m be Element of N; :: thesis: ex n being Element of (N | i) st
for p being Element of (N | i) st n <= p holds
m <= (incl ((N | i),N)) . p
consider n9 being Element of N such that
A3: n9 >= i and
A4: n9 >= m by YELLOW_6:def 3;
reconsider n = n9 as Element of (N | i) by A3, WAYBEL_9:def 7;
take n ; :: thesis: for p being Element of (N | i) st n <= p holds
m <= (incl ((N | i),N)) . p
let p be Element of (N | i); :: thesis: ( n <= p implies m <= (incl ((N | i),N)) . p )
reconsider p9 = p as Element of N by A1, YELLOW_0:58;
assume n <= p ; :: thesis: m <= (incl ((N | i),N)) . p
then n9 <= p9 by A1, YELLOW_0:59;
then m <= p9 by A4, YELLOW_0:def 2;
hence m <= (incl ((N | i),N)) . p by A2, FUNCT_1:18; :: thesis: verum