let S be 1-sorted ; :: thesis: for N being NetStr over S
for M being SubNetStr of N
for x, y being Element of N
for i, j being Element of M st x = i & y = j & i <= j holds
x <= y
let N be NetStr over S; :: thesis: for M being SubNetStr of N
for x, y being Element of N
for i, j being Element of M st x = i & y = j & i <= j holds
x <= y
let M be SubNetStr of N; :: thesis: for x, y being Element of N
for i, j being Element of M st x = i & y = j & i <= j holds
x <= y
let x, y be Element of N; :: thesis: for i, j being Element of M st x = i & y = j & i <= j holds
x <= y
let i, j be Element of M; :: thesis: ( x = i & y = j & i <= j implies x <= y )
assume that
A1: ( x = i & y = j ) and
A2: i <= j ; :: thesis: x <= y
reconsider M = M as SubRelStr of N by Def6;
reconsider i9 = i, j9 = j as Element of M ;
i9 <= j9 by A2;
hence x <= y by A1, YELLOW_0:59; :: thesis: verum