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 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;
assume A4: for x, y being object st x in X & [y,x] in the InternalRel of R holds
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