hereby :: thesis: ( ( for x, y being set 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 set st x in X & [y,x] in the InternalRel of R holds
y in Xlet x,
y be
set ;
:: 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 Xreconsider x' =
x,
y' =
y as
Element of
R by A3, ZFMISC_1:106;
y' <= x'
by A3, ORDERS_2:def 9;
hence
y in X
by A1, A2, WAYBEL_0:def 19;
:: thesis: verum
end;
assume A4:
for x, y being set 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 9;
hence
y in X
by A4, A5; :: thesis: verum