let S be 1-sorted ; :: thesis: for N being NetStr of 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 of 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 Def8;
reconsider i' = i, j' = j as Element of M ;
i' <= j' by A2;
hence x <= y by A1, YELLOW_0:60; :: thesis: verum