let L be RelStr ; :: thesis: for S being full SubRelStr of L
for a, b being Element of L
for x, y being Element of S st x = a & y = b & a <= b & x in the carrier of S holds
x <= y
let S be full SubRelStr of L; :: thesis: for a, b being Element of L
for x, y being Element of S st x = a & y = b & a <= b & x in the carrier of S holds
x <= y
let a, b be Element of L; :: thesis: for x, y being Element of S st x = a & y = b & a <= b & x in the carrier of S holds
x <= y
let x, y be Element of S; :: thesis: ( x = a & y = b & a <= b & x in the carrier of S implies x <= y )
assume A1: ( x = a & y = b ) ; :: thesis: ( not a <= b or not x in the carrier of S or x <= y )
assume A2: [a,b] in the InternalRel of L ; :: according to ORDERS_2:def 5 :: thesis: ( not x in the carrier of S or x <= y )
A3: the InternalRel of S = the InternalRel of L |_2 the carrier of S by Def14;
assume x in the carrier of S ; :: thesis: x <= y
then [x,y] in [: the carrier of S, the carrier of S:] by ZFMISC_1:87;
hence [x,y] in the InternalRel of S by A1, A3, A2, XBOOLE_0:def 4; :: according to ORDERS_2:def 5 :: thesis: verum