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 ) )

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

hence
N * p is subnet of N
by YELLOW_6:def 9; :: thesis: verum
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;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