let T be non empty 1-sorted ; :: thesis: for N1, N2, N3 being net of T st N1 is subnet of N2 & N2 is subnet of N3 holds
N1 is subnet of N3
let N1, N2, N3 be net of T; :: thesis: ( N1 is subnet of N2 & N2 is subnet of N3 implies N1 is subnet of N3 )
given f being Function of N1,N2 such that A1: the mapping of N1 = the mapping of N2 * f and
A2: for m being Element of N2 ex n being Element of N1 st
for p being Element of N1 st n <= p holds
m <= f . p ; :: according to YELLOW_6:def 9 :: thesis: ( not N2 is subnet of N3 or N1 is subnet of N3 )
given g being Function of N2,N3 such that A3: the mapping of N2 = the mapping of N3 * g and
A4: for m being Element of N3 ex n being Element of N2 st
for p being Element of N2 st n <= p holds
m <= g . p ; :: according to YELLOW_6:def 9 :: thesis: N1 is subnet of N3
take g * f ; :: according to YELLOW_6:def 9 :: thesis: ( the mapping of N1 = the mapping of N3 * (g * f) & ( for m being Element of N3 ex n being Element of N1 st
for p being Element of N1 st n <= p holds
m <= (g * f) . p ) )
thus the mapping of N1 = the mapping of N3 * (g * f) by A1, A3, RELAT_1:36; :: thesis: for m being Element of N3 ex n being Element of N1 st
for p being Element of N1 st n <= p holds
m <= (g * f) . p
let m be Element of N3; :: thesis: ex n being Element of N1 st
for p being Element of N1 st n <= p holds
m <= (g * f) . p
consider m1 being Element of N2 such that
A5: for p being Element of N2 st m1 <= p holds
m <= g . p by A4;
consider n being Element of N1 such that
A6: for p being Element of N1 st n <= p holds
m1 <= f . p by A2;
take n ; :: thesis: for p being Element of N1 st n <= p holds
m <= (g * f) . p
let p be Element of N1; :: thesis: ( n <= p implies m <= (g * f) . p )
assume n <= p ; :: thesis: m <= (g * f) . p
then m <= g . (f . p) by A5, A6;
hence m <= (g * f) . p by FUNCT_2:15; :: thesis: verum