let L1, L2 be non empty 1-sorted ; :: thesis: ( the carrier of L1 = the carrier of L2 implies for N1 being net of L1
for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
for S1 being subnet of N1 ex S2 being strict subnet of N2 st
( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & the mapping of S1 = the mapping of S2 ) )
assume A1: the carrier of L1 = the carrier of L2 ; :: thesis: for N1 being net of L1
for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
for S1 being subnet of N1 ex S2 being strict subnet of N2 st
( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & the mapping of S1 = the mapping of S2 )
let N1 be net of L1; :: thesis: for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
for S1 being subnet of N1 ex S2 being strict subnet of N2 st
( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & the mapping of S1 = the mapping of S2 )
let N2 be net of L2; :: thesis: ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 implies for S1 being subnet of N1 ex S2 being strict subnet of N2 st
( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & the mapping of S1 = the mapping of S2 ) )
assume that
A2: RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) and
A3: the mapping of N1 = the mapping of N2 ; :: thesis: for S1 being subnet of N1 ex S2 being strict subnet of N2 st
( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & the mapping of S1 = the mapping of S2 )
let S1 be subnet of N1; :: thesis: ex S2 being strict subnet of N2 st
( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & the mapping of S1 = the mapping of S2 )
consider S2 being strict NetStr over L2 such that
A4: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) and
A5: the mapping of S1 = the mapping of S2 by A1, Th2;
reconsider S2 = S2 as strict net of L2 by A4;
consider f being Function of S1,N1 such that
A6: the mapping of S1 = the mapping of N1 * f and
A7: for B5 being Element of N1 ex B6 being Element of S1 st
for B7 being Element of S1 st B6 <= B7 holds
B5 <= f . B7 by YELLOW_6:def 9;
reconsider g = f as Function of S2,N2 by A2, A4;
S2 is subnet of N2
proof
take g ; :: according to YELLOW_6:def 9 :: thesis: ( the mapping of S2 = the mapping of N2 * g & ( for b1 being Element of the carrier of N2 ex b2 being Element of the carrier of S2 st
for b3 being Element of the carrier of S2 holds
( not b2 <= b3 or b1 <= g . b3 ) ) )
thus the mapping of S2 = the mapping of N2 * g by A3, A5, A6; :: thesis: for b1 being Element of the carrier of N2 ex b2 being Element of the carrier of S2 st
for b3 being Element of the carrier of S2 holds
( not b2 <= b3 or b1 <= g . b3 )
let B2 be Element of N2; :: thesis: ex b1 being Element of the carrier of S2 st
for b2 being Element of the carrier of S2 holds
( not b1 <= b2 or B2 <= g . b2 )
reconsider b2 = B2 as Element of N1 by A2;
consider b6 being Element of S1 such that
A8: for b7 being Element of S1 st b6 <= b7 holds
b2 <= f . b7 by A7;
reconsider B3 = b6 as Element of S2 by A4;
take B3 ; :: thesis: for b1 being Element of the carrier of S2 holds
( not B3 <= b1 or B2 <= g . b1 )
let B4 be Element of S2; :: thesis: ( not B3 <= B4 or B2 <= g . B4 )
reconsider b4 = B4 as Element of S1 by A4;
assume B3 <= B4 ; :: thesis: B2 <= g . B4
then b6 <= b4 by A4, YELLOW_0:1;
then b2 <= f . b4 by A8;
hence B2 <= g . B4 by A2, YELLOW_0:1; :: thesis: verum
end;
hence ex S2 being strict subnet of N2 st
( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & the mapping of S1 = the mapping of S2 ) by A4, A5; :: thesis: verum