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
for i, j being Element of 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
for i, j being Element of 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
for i, j being Element of st x = i & y = j & x <= y holds
i <= j
let x, y be Element of ; :: thesis: for i, j being Element of st x = i & y = j & x <= y holds
i <= j
let i, j be Element of ; :: 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 Def9;
reconsider i' = i, j' = j as Element of ;
i' <= j' by A1, YELLOW_0:61;
hence i <= j ; :: thesis: verum