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 9;
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:94; :: 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 n' being Element of N such that
A3: ( n' >= i & n' >= m ) by YELLOW_6:def 5;
reconsider n = n' 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 p' = p as Element of N by A1, YELLOW_0:59;
assume n <= p ; :: thesis: m <= (incl (N | i),N) . p
then n' <= p' by A1, YELLOW_0:60;
then m <= p' by A3, YELLOW_0:def 2;
hence m <= (incl (N | i),N) . p by A2, FUNCT_1:35; :: thesis: verum