let S be 1-sorted ; :: thesis: for N being non empty NetStr of 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 of 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 that
A1: ( x = i & y = j ) and
A2: x <= y ; :: thesis: i <= j
reconsider M = M as non empty full SubRelStr of N by Def9;
reconsider i' = i, j' = j as Element of M ;
i' <= j' by A1, A2, YELLOW_0:61;
hence i <= j ; :: thesis: verum