let L be RelStr ; :: thesis: for S being SubRelStr of L
for a, b being Element of L
for x, y being Element of S st x = a & y = b & x <= y holds
a <= b
let S be SubRelStr of L; :: thesis: for a, b being Element of L
for x, y being Element of S st x = a & y = b & x <= y holds
a <= b
let a, b be Element of L; :: thesis: for x, y being Element of S st x = a & y = b & x <= y holds
a <= b
let x, y be Element of S; :: thesis: ( x = a & y = b & x <= y implies a <= b )
assume A1: ( x = a & y = b ) ; :: thesis: ( not x <= y or a <= b )
A2: the InternalRel of S c= the InternalRel of L by Def13;
assume [x,y] in the InternalRel of S ; :: according to ORDERS_2:def 9 :: thesis: a <= b
hence [a,b] in the InternalRel of L by A1, A2; :: according to ORDERS_2:def 9 :: thesis: verum