let x, y, z be Element of REAL+ ; ( x <=' y & y <=' z implies x <=' z )
assume that
A1:
x <=' y
and
A2:
y <=' z
; x <=' z
per cases
( ( x in RAT+ & y in RAT+ & z in RAT+ ) or ( x in RAT+ & y in RAT+ & not z in RAT+ ) or ( x in RAT+ & not y in RAT+ & z in RAT+ ) or ( x in RAT+ & not y in RAT+ & not z in RAT+ ) or ( not x in RAT+ & y in RAT+ & z in RAT+ ) or ( not x in RAT+ & y in RAT+ & not z in RAT+ ) or ( not x in RAT+ & not y in RAT+ & z in RAT+ ) or ( not x in RAT+ & not y in RAT+ & not z in RAT+ ) )
;
suppose that A6:
x in RAT+
and A7:
y in RAT+
and A8:
not
z in RAT+
;
x <=' zreconsider y9 =
y as
Element of
RAT+ by A7;
reconsider x9 =
x as
Element of
RAT+ by A6;
A9:
x9 <=' y9
by A1, Lm14;
z in REAL+
;
then
z in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) }
by A8, Lm3, XBOOLE_0:def 3;
then consider C being
Subset of
RAT+ such that A10:
z = C
and A11:
for
r being
Element of
RAT+ st
r in C holds
( ( for
s being
Element of
RAT+ st
s <=' r holds
s in C ) & ex
s being
Element of
RAT+ st
(
s in C &
r < s ) )
;
y in C
by A2, A7, A8, A10, Def5;
then
x9 in C
by A11, A9;
hence
x <=' z
by A8, A10, Def5;
verum end; suppose that A17:
x in RAT+
and A18:
not
y in RAT+
and A19:
not
z in RAT+
;
x <=' zreconsider x9 =
x as
Element of
RAT+ by A17;
y in REAL+
;
then
y in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) }
by A18, Lm3, XBOOLE_0:def 3;
then consider B being
Subset of
RAT+ such that A20:
y = B
and
for
r being
Element of
RAT+ st
r in B holds
( ( for
s being
Element of
RAT+ st
s <=' r holds
s in B ) & ex
s being
Element of
RAT+ st
(
s in B &
r < s ) )
;
A21:
x9 in B
by A1, A18, A20, Def5;
z in REAL+
;
then
z in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) }
by A19, Lm3, XBOOLE_0:def 3;
then consider C being
Subset of
RAT+ such that A22:
z = C
and
for
r being
Element of
RAT+ st
r in C holds
( ( for
s being
Element of
RAT+ st
s <=' r holds
s in C ) & ex
s being
Element of
RAT+ st
(
s in C &
r < s ) )
;
B c= C
by A2, A18, A19, A20, A22, Def5;
hence
x <=' z
by A19, A22, A21, Def5;
verum end; suppose that A29:
not
x in RAT+
and A30:
y in RAT+
and A31:
not
z in RAT+
;
x <=' z
x in REAL+
;
then
x in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) }
by A29, Lm3, XBOOLE_0:def 3;
then consider A being
Subset of
RAT+ such that A32:
x = A
and A33:
for
r being
Element of
RAT+ st
r in A holds
( ( for
s being
Element of
RAT+ st
s <=' r holds
s in A ) & ex
s being
Element of
RAT+ st
(
s in A &
r < s ) )
;
A34:
not
y in A
by A1, A29, A32, Def5;
reconsider y9 =
y as
Element of
RAT+ by A30;
z in REAL+
;
then
z in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) }
by A31, Lm3, XBOOLE_0:def 3;
then consider C being
Subset of
RAT+ such that A35:
z = C
and A36:
for
r being
Element of
RAT+ st
r in C holds
( ( for
s being
Element of
RAT+ st
s <=' r holds
s in C ) & ex
s being
Element of
RAT+ st
(
s in C &
r < s ) )
;
A37:
y in C
by A2, A30, A31, A35, Def5;
A c= C
hence
x <=' z
by A29, A31, A32, A35, Def5;
verum end; suppose that A39:
not
x in RAT+
and A40:
not
y in RAT+
and A41:
z in RAT+
;
x <=' zreconsider z9 =
z as
Element of
RAT+ by A41;
x in REAL+
;
then
x in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) }
by A39, Lm3, XBOOLE_0:def 3;
then consider A being
Subset of
RAT+ such that A42:
x = A
and
for
r being
Element of
RAT+ st
r in A holds
( ( for
s being
Element of
RAT+ st
s <=' r holds
s in A ) & ex
s being
Element of
RAT+ st
(
s in A &
r < s ) )
;
y in REAL+
;
then
y in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) }
by A40, Lm3, XBOOLE_0:def 3;
then consider B being
Subset of
RAT+ such that A43:
y = B
and
for
r being
Element of
RAT+ st
r in B holds
( ( for
s being
Element of
RAT+ st
s <=' r holds
s in B ) & ex
s being
Element of
RAT+ st
(
s in B &
r < s ) )
;
A c= B
by A1, A39, A40, A42, A43, Def5;
then
not
z9 in A
by A2, A40, A43, Def5;
hence
x <=' z
by A39, A42, Def5;
verum end; suppose that A44:
not
x in RAT+
and A45:
not
y in RAT+
and A46:
not
z in RAT+
;
x <=' z
z in REAL+
;
then
z in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) }
by A46, Lm3, XBOOLE_0:def 3;
then consider C being
Subset of
RAT+ such that A47:
z = C
and
for
r being
Element of
RAT+ st
r in C holds
( ( for
s being
Element of
RAT+ st
s <=' r holds
s in C ) & ex
s being
Element of
RAT+ st
(
s in C &
r < s ) )
;
y in REAL+
;
then
y in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) }
by A45, Lm3, XBOOLE_0:def 3;
then consider B being
Subset of
RAT+ such that A48:
y = B
and
for
r being
Element of
RAT+ st
r in B holds
( ( for
s being
Element of
RAT+ st
s <=' r holds
s in B ) & ex
s being
Element of
RAT+ st
(
s in B &
r < s ) )
;
A49:
B c= C
by A2, A45, A46, A48, A47, Def5;
x in REAL+
;
then
x in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) }
by A44, Lm3, XBOOLE_0:def 3;
then consider A being
Subset of
RAT+ such that A50:
x = A
and
for
r being
Element of
RAT+ st
r in A holds
( ( for
s being
Element of
RAT+ st
s <=' r holds
s in A ) & ex
s being
Element of
RAT+ st
(
s in A &
r < s ) )
;
A c= B
by A1, A44, A45, A50, A48, Def5;
then
A c= C
by A49;
hence
x <=' z
by A44, A46, A50, A47, Def5;
verum end; end;