let x, y be Element of REAL+ ; :: thesis: ( y < x implies ex z being Element of REAL+ st
( z in RAT+ & z < x & y < z ) )
assume A1: y < x ; :: thesis: ex z being Element of REAL+ st
( z in RAT+ & z < x & y < z )

per cases ( ( x in RAT+ & y in RAT+ ) or ( not x in RAT+ & y in RAT+ ) or ( x in RAT+ & not y in RAT+ ) or ( not x in RAT+ & not y in RAT+ ) ) ;

suppose ( x in RAT+ & y in RAT+ ) ; :: thesis: ex z being Element of REAL+ st
( z in RAT+ & z < x & y < z )

then reconsider x9 = x, y9 = y as Element of RAT+ ;
y9 < x9 by A1, Lm14;
then consider z9 being Element of RAT+ such that
A2: ( y9 < z9 & z9 < x9 ) by ARYTM_3:93;
reconsider z = z9 as Element of REAL+ by Th1;
take z ; :: thesis: ( z in RAT+ & z < x & y < z )
thus ( z in RAT+ & z < x & y < z ) by A2, Lm14; :: thesis: verum

end;

suppose that A3: not x in RAT+ and
A4: y in RAT+ ; :: thesis: ex z being Element of REAL+ st
( z in RAT+ & z < x & y < z )

reconsider y9 = y as Element of RAT+ by A4;
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 A3, Lm3, XBOOLE_0:def 3;
then consider A being Subset of RAT+ such that
A5: x = A and
A6: 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 ) ) ;
y9 in x by A1, A3, Def5;
then consider s being Element of RAT+ such that
A7: s in A and
A8: y9 < s by A5, A6;
reconsider z = s as Element of REAL+ by Th1;
take z ; :: thesis: ( z in RAT+ & z < x & y < z )
thus z in RAT+ ; :: thesis: ( z < x & y < z )
thus z < x by A3, A5, A7, Def5; :: thesis: y < z
thus y < z by A8, Lm14; :: thesis: verum

end;

suppose that A9: x in RAT+ and
A10: not y in RAT+ ; :: thesis: ex z being Element of REAL+ st
( z in RAT+ & z < x & y < z )

reconsider x9 = x as Element of RAT+ by A9;
A11: not x9 in y by A1, A10, Def5;
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 A10, Lm3, XBOOLE_0:def 3;
then consider B being Subset of RAT+ such that
A12: y = B and
A13: 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 ) ) ;
B <> {} by A10, A12;
then consider y1 being Element of RAT+ such that
A14: y1 in B by SUBSET_1:4;
{} <=' y1 by ARYTM_3:64;
then A15: x9 <> {} by A12, A13, A11, A14;
ex z9 being Element of RAT+ st
( z9 < x9 & not z9 in y )

proof

set C = { s where s is Element of RAT+ : s < x9 } ;
assume A16: for z9 being Element of RAT+ holds
( not z9 < x9 or z9 in y ) ; :: thesis: contradiction
y = { s where s is Element of RAT+ : s < x9 }

proof

thus y c= { s where s is Element of RAT+ : s < x9 } :: according to XBOOLE_0:def 10 :: thesis: { s where s is Element of RAT+ : s < x9 } c= y

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in y or e in { s where s is Element of RAT+ : s < x9 } )
assume A17: e in y ; :: thesis: e in { s where s is Element of RAT+ : s < x9 }
then reconsider z9 = e as Element of RAT+ by A12;
not x9 <=' z9 by A12, A13, A11, A17;
hence e in { s where s is Element of RAT+ : s < x9 } ; :: thesis: verum

end;

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { s where s is Element of RAT+ : s < x9 } or e in y )
assume e in { s where s is Element of RAT+ : s < x9 } ; :: thesis: e in y
then ex s being Element of RAT+ st
( e = s & s < x9 ) ;
hence e in y by A16; :: thesis: verum

end;

then y in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by A15;
hence contradiction by XBOOLE_0:def 5; :: thesis: verum

end;

then consider z9 being Element of RAT+ such that
A18: z9 < x9 and
A19: not z9 in y ;
reconsider z = z9 as Element of REAL+ by Th1;
take z ; :: thesis: ( z in RAT+ & z < x & y < z )
thus z in RAT+ ; :: thesis: ( z < x & y < z )
thus z < x by A18, Lm14; :: thesis: y < z
thus y < z by A10, A19, Def5; :: thesis: verum

end;

suppose that A20: not x in RAT+ and
A21: not y in RAT+ ; :: thesis: ex z being Element of REAL+ st
( z in RAT+ & z < x & y < z )

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 A21, Lm3, XBOOLE_0:def 3;
then consider B being Subset of RAT+ such that
A22: 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 ) ) ;
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 A20, Lm3, XBOOLE_0:def 3;
then consider A being Subset of RAT+ such that
A23: 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 ) ) ;
not x c= y by A1, A20, A21, Def5;
then consider z9 being Element of RAT+ such that
A24: z9 in A and
A25: not z9 in B by A23, A22;
reconsider z = z9 as Element of REAL+ by Th1;
take z ; :: thesis: ( z in RAT+ & z < x & y < z )
thus z in RAT+ ; :: thesis: ( z < x & y < z )
thus z < x by A20, A23, A24, Def5; :: thesis: y < z
thus y < z by A21, A22, A25, Def5; :: thesis: verum

end;

end;