let S be 1-sorted ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: for i, j being Element of M st x = i & y = j & x <= y holds
i <= j
let i, j be Element of M; :: thesis: ( x = i & y = j & x <= y implies i <= j )
assume A1: ( x = i & y = j & x <= y ) ; :: thesis: 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 ; :: thesis: verum