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