let L be non empty 1-sorted ; :: thesis: for N being net of L
for p being greater_or_equal_to_id Function of N,N holds N * p is subnet of N
let N be net of L; :: thesis: for p being greater_or_equal_to_id Function of N,N holds N * p is subnet of N
let p be greater_or_equal_to_id Function of N,N; :: thesis: N * p is subnet of N
ex f being Function of (N * p),N st
( the mapping of (N * p) = the mapping of N * f & ( for m being Element of N ex n being Element of (N * p) st
for k being Element of (N * p) st n <= k holds
m <= f . k ) )

proof

the carrier of (N * p) = the carrier of N by Th6;
then reconsider f = p as Function of (N * p),N ;
take f ; :: thesis: ( the mapping of (N * p) = the mapping of N * f & ( for m being Element of N ex n being Element of (N * p) st
for k being Element of (N * p) st n <= k holds
m <= f . k ) )
thus the mapping of (N * p) = the mapping of N * f by Def2; :: thesis: for m being Element of N ex n being Element of (N * p) st
for k being Element of (N * p) st n <= k holds
m <= f . k
let m be Element of N; :: thesis: ex n being Element of (N * p) st
for k being Element of (N * p) st n <= k holds
m <= f . k
reconsider n = m as Element of (N * p) by Th6;
take n ; :: thesis: for k being Element of (N * p) st n <= k holds
m <= f . k
let k be Element of (N * p); :: thesis: ( n <= k implies m <= f . k )
assume A1: n <= k ; :: thesis: m <= f . k
reconsider k1 = k as Element of N by Th6;
A2: k1 <= p . k1 by Def1;
RelStr(# the carrier of (N * p), the InternalRel of (N * p) #) = RelStr(# the carrier of N, the InternalRel of N #) by Def2;
then m <= k1 by A1, YELLOW_0:1;
hence m <= f . k by A2, YELLOW_0:def 2; :: thesis: verum

end;

hence N * p is subnet of N by YELLOW_6:def 9; :: thesis: verum