let B be set ; ( B 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 ) ) } & B <> {} implies ex r being Element of RAT+ st
( r in B & r <> {} ) )
assume that
A1:
B 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 ) ) }
and
A2:
B <> {}
; ex r being Element of RAT+ st
( r in B & r <> {} )
consider A being Subset of RAT+ such that
A3:
B = A
and
A4:
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 A1;
consider r0 being Element of RAT+ such that
A5:
r0 in A
by A2, A3, SUBSET_1:4;
consider r1 being Element of RAT+ such that
A6:
r1 in A
and
A7:
r0 < r1
by A4, A5;
A8:
( r1 <> {} or r0 <> {} )
by A7;
for r, s being Element of RAT+ st r in A & s <=' r holds
s in A
by A4;
then consider r1, r2, r3 being Element of RAT+ such that
A9:
( r1 in A & r2 in A )
and
r3 in A
and
A10:
r1 <> r2
and
r2 <> r3
and
r3 <> r1
by A5, A6, A8, ARYTM_3:75;
( r1 <> {} or r2 <> {} )
by A10;
hence
ex r being Element of RAT+ st
( r in B & r <> {} )
by A3, A9; verum