let L be non empty 1-sorted ; :: thesis: for N, M being net of L st NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) = NetStr(# the carrier of M, the InternalRel of M, the mapping of M #) holds

M is subnet of N

let N, M be net of L; :: thesis: ( NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) = NetStr(# the carrier of M, the InternalRel of M, the mapping of M #) implies M is subnet of N )

assume A1: NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) = NetStr(# the carrier of M, the InternalRel of M, the mapping of M #) ; :: thesis: M is subnet of N

A2: N is subnet of N by YELLOW_6:14;

ex f being Function of M,N st

( the mapping of M = the mapping of N * f & ( for m being Element of N ex n being Element of M st

for p being Element of M st n <= p holds

m <= f . p ) )

M is subnet of N

let N, M be net of L; :: thesis: ( NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) = NetStr(# the carrier of M, the InternalRel of M, the mapping of M #) implies M is subnet of N )

assume A1: NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) = NetStr(# the carrier of M, the InternalRel of M, the mapping of M #) ; :: thesis: M is subnet of N

A2: N is subnet of N by YELLOW_6:14;

ex f being Function of M,N st

( the mapping of M = the mapping of N * f & ( for m being Element of N ex n being Element of M st

for p being Element of M st n <= p holds

m <= f . p ) )

proof

hence
M is subnet of N
by YELLOW_6:def 9; :: thesis: verum
consider f being Function of N,N such that

A3: the mapping of N = the mapping of N * f and

A4: for m being Element of N ex n being Element of N st

for p being Element of N st n <= p holds

m <= f . p by A2, YELLOW_6:def 9;

reconsider f2 = f as Function of M,N by A1;

take f2 ; :: thesis: ( the mapping of M = the mapping of N * f2 & ( for m being Element of N ex n being Element of M st

for p being Element of M st n <= p holds

m <= f2 . p ) )

thus the mapping of M = the mapping of N * f2 by A1, A3; :: thesis: for m being Element of N ex n being Element of M st

for p being Element of M st n <= p holds

m <= f2 . p

let m be Element of N; :: thesis: ex n being Element of M st

for p being Element of M st n <= p holds

m <= f2 . p

consider n being Element of N such that

A5: for p being Element of N st n <= p holds

m <= f . p by A4;

reconsider n2 = n as Element of M by A1;

take n2 ; :: thesis: for p being Element of M st n2 <= p holds

m <= f2 . p

let p be Element of M; :: thesis: ( n2 <= p implies m <= f2 . p )

reconsider p1 = p as Element of N by A1;

assume n2 <= p ; :: thesis: m <= f2 . p

then [n2,p] in the InternalRel of M by ORDERS_2:def 5;

then n <= p1 by A1, ORDERS_2:def 5;

hence m <= f2 . p by A5; :: thesis: verum

end;A3: the mapping of N = the mapping of N * f and

A4: for m being Element of N ex n being Element of N st

for p being Element of N st n <= p holds

m <= f . p by A2, YELLOW_6:def 9;

reconsider f2 = f as Function of M,N by A1;

take f2 ; :: thesis: ( the mapping of M = the mapping of N * f2 & ( for m being Element of N ex n being Element of M st

for p being Element of M st n <= p holds

m <= f2 . p ) )

thus the mapping of M = the mapping of N * f2 by A1, A3; :: thesis: for m being Element of N ex n being Element of M st

for p being Element of M st n <= p holds

m <= f2 . p

let m be Element of N; :: thesis: ex n being Element of M st

for p being Element of M st n <= p holds

m <= f2 . p

consider n being Element of N such that

A5: for p being Element of N st n <= p holds

m <= f . p by A4;

reconsider n2 = n as Element of M by A1;

take n2 ; :: thesis: for p being Element of M st n2 <= p holds

m <= f2 . p

let p be Element of M; :: thesis: ( n2 <= p implies m <= f2 . p )

reconsider p1 = p as Element of N by A1;

assume n2 <= p ; :: thesis: m <= f2 . p

then [n2,p] in the InternalRel of M by ORDERS_2:def 5;

then n <= p1 by A1, ORDERS_2:def 5;

hence m <= f2 . p by A5; :: thesis: verum