hereby :: thesis: ( ( for x, y being object st x in X & [y,x] in the InternalRel of R holds

y in X ) implies X is lower )

assume A4:
for x, y being object st x in X & [y,x] in the InternalRel of R holds y in X ) implies X is lower )

assume A1:
X is lower
; :: thesis: for x, y being object st x in X & [y,x] in the InternalRel of R holds

y in X

let x, y be object ; :: thesis: ( x in X & [y,x] in the InternalRel of R implies y in X )

assume that

A2: x in X and

A3: [y,x] in the InternalRel of R ; :: thesis: y in X

reconsider x9 = x, y9 = y as Element of R by A3, ZFMISC_1:87;

y9 <= x9 by A3, ORDERS_2:def 5;

hence y in X by A1, A2; :: thesis: verum

end;y in X

let x, y be object ; :: thesis: ( x in X & [y,x] in the InternalRel of R implies y in X )

assume that

A2: x in X and

A3: [y,x] in the InternalRel of R ; :: thesis: y in X

reconsider x9 = x, y9 = y as Element of R by A3, ZFMISC_1:87;

y9 <= x9 by A3, ORDERS_2:def 5;

hence y in X by A1, A2; :: thesis: verum

y in X ; :: thesis: X is lower

let x, y be Element of R; :: according to WAYBEL_0:def 19 :: thesis: ( not x in X or not y <= x or y in X )

assume A5: x in X ; :: thesis: ( not y <= x or y in X )

assume y <= x ; :: thesis: y in X

then [y,x] in the InternalRel of R by ORDERS_2:def 5;

hence y in X by A4, A5; :: thesis: verum