let T be 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 )
let N be 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 i be Element of N; ( 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
; incl ((N | i),N) is Embedding of N | i,N
thus
N | i is subnet of N
; WAYBEL21:def 3 ( 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; 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; 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
; for p being Element of (N | i) st n <= p holds
m <= (incl ((N | i),N)) . p
let p be Element of (N | i); ( n <= p implies m <= (incl ((N | i),N)) . p )
reconsider p9 = p as Element of N by A1, YELLOW_0:58;
assume
n <= p
; 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; verum