let t be Element of RAT+ ; :: thesis: ( { s where s is Element of RAT+ : s < t } in RAT+ iff t = {} )

hereby :: thesis: ( t = {} implies { s where s is Element of RAT+ : s < t } in RAT+ )

assume A1: ( { s where s is Element of RAT+ : s < t } in RAT+ & t <> {} ) ; :: thesis: contradiction
then consider r being Element of RAT+ such that
A2: r < t and
A3: not r in omega by Th80;
{} <=' t by Th71;
then {} < t by A1, Th73;
then A4: {} in { s where s is Element of RAT+ : s < t } ;
r in { s where s is Element of RAT+ : s < t } by A2;
then ( { s where s is Element of RAT+ : s < t } in omega implies r is Ordinal ) ;
then ex i, j being Element of omega st
( { s where s is Element of RAT+ : s < t } = [i,j] & i,j are_relative_prime & j <> {} & j <> 1 ) by A1, A3, Th35, Th37;
hence contradiction by A4, TARSKI:def 2; :: thesis: verum

end;

assume A5: t = {} ; :: thesis: { s where s is Element of RAT+ : s < t } in RAT+
{ s where s is Element of RAT+ : s < t } c= {}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { s where s is Element of RAT+ : s < t } or a in {} )
assume a in { s where s is Element of RAT+ : s < t } ; :: thesis: a in {}
then ex s being Element of RAT+ st
( a = s & s < t ) ;
hence a in {} by A5, Th71; :: thesis: verum

end;

then { s where s is Element of RAT+ : s < t } = {} ;
hence { s where s is Element of RAT+ : s < t } in RAT+ ; :: thesis: verum