let y, x 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 that A2: x in RAT+ and
A3: y in RAT+ ; :: thesis: ex z being Element of REAL+ st
( z in RAT+ & z < x & y < z )

reconsider x' = x, y' = y as Element of RAT+ by A2, A3;
y' < x' by A1, Lm14;
then consider z' being Element of RAT+ such that
A4: ( y' < z' & z' < x' ) by ARYTM_3:101;
z' in RAT+ ;
then reconsider z = z' 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 A4, Lm14; :: thesis: verum

end;

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

end;

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

proof

assume A18: for z' being Element of RAT+ holds
( not z' < x' or z' in y ) ; :: thesis: contradiction
set C = { s where s is Element of RAT+ : s < x' } ;
y = { s where s is Element of RAT+ : s < x' }

proof

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

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in y or e in { s where s is Element of RAT+ : s < x' } )
assume A19: e in y ; :: thesis: e in { s where s is Element of RAT+ : s < x' }
then reconsider z' = e as Element of RAT+ by A13;
not x' <=' z' by A13, A14, A15, A19;
hence e in { s where s is Element of RAT+ : s < x' } ; :: thesis: verum

end;

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { s where s is Element of RAT+ : s < x' } or e in y )
assume e in { s where s is Element of RAT+ : s < x' } ; :: thesis: e in y
then consider s being Element of RAT+ such that
A20: e = s and
A21: s < x' ;
thus e in y by A18, A20, A21; :: thesis: verum

end;

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

end;

then consider z' being Element of RAT+ such that
A22: z' < x' and
A23: not z' in y ;
z' in RAT+ ;
then reconsider z = z' 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 A22, Lm14; :: thesis: y < z
thus y < z by A12, A23, Def5; :: thesis: verum

end;

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

A26: not x c= y by A1, A24, A25, 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 A24, Lm3, XBOOLE_0:def 3;
then consider A being Subset of RAT+ such that
A27: 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 A25, Lm3, XBOOLE_0:def 3;
then consider B being Subset of RAT+ such that
A28: 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 ) ) ;
consider z' being Element of RAT+ such that
A29: z' in A and
A30: not z' in B by A26, A27, A28, SUBSET_1:7;
z' in RAT+ ;
then reconsider z = z' 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 A24, A27, A29, Def5; :: thesis: y < z
thus y < z by A25, A28, A30, Def5; :: thesis: verum

end;

end;