let S be 1-sorted ; for N being non empty NetStr over S
for M being non empty full SubNetStr of N
for x, y being Element of N
for i, j being Element of M st x = i & y = j & x <= y holds
i <= j
let N be non empty NetStr over S; for M being non empty full SubNetStr of N
for x, y being Element of N
for i, j being Element of M st x = i & y = j & x <= y holds
i <= j
let M be non empty full SubNetStr of N; for x, y being Element of N
for i, j being Element of M st x = i & y = j & x <= y holds
i <= j
let x, y be Element of N; for i, j being Element of M st x = i & y = j & x <= y holds
i <= j
let i, j be Element of M; ( x = i & y = j & x <= y implies i <= j )
assume A1:
( x = i & y = j & x <= y )
; i <= j
reconsider M = M as non empty full SubRelStr of N by Def7;
reconsider i9 = i, j9 = j as Element of M ;
i9 <= j9
by A1, YELLOW_0:60;
hence
i <= j
; verum