let A be Subset of RAT+; ( ex t being Element of RAT+ st
( t in A & t <> {} ) & ( for r, s being Element of RAT+ st r in A & s <=' r holds
s in A ) implies ex r1, r2, r3 being Element of RAT+ st
( r1 in A & r2 in A & r3 in A & r1 <> r2 & r2 <> r3 & r3 <> r1 ) )
given t being Element of RAT+ such that A1:
t in A
and
A2:
t <> {}
; ( ex r, s being Element of RAT+ st
( r in A & s <=' r & not s in A ) or ex r1, r2, r3 being Element of RAT+ st
( r1 in A & r2 in A & r3 in A & r1 <> r2 & r2 <> r3 & r3 <> r1 ) )
assume A3:
for r, s being Element of RAT+ st r in A & s <=' r holds
s in A
; ex r1, r2, r3 being Element of RAT+ st
( r1 in A & r2 in A & r3 in A & r1 <> r2 & r2 <> r3 & r3 <> r1 )
consider x being Element of RAT+ such that
A4:
t = x + x
by Th60;
take
{}
; ex r2, r3 being Element of RAT+ st
( {} in A & r2 in A & r3 in A & {} <> r2 & r2 <> r3 & r3 <> {} )
take
x
; ex r3 being Element of RAT+ st
( {} in A & x in A & r3 in A & {} <> x & x <> r3 & r3 <> {} )
take
t
; ( {} in A & x in A & t in A & {} <> x & x <> t & t <> {} )
x <=' t
by A4;
hence
( {} in A & x in A & t in A )
by A1, A3, Th64; ( {} <> x & x <> t & t <> {} )
thus
{} <> x
by A2, A4, Th50; ( x <> t & t <> {} )
hereby t <> {}
assume
x = t
;
contradictionthen
t + {} = t + t
by A4, Th50;
hence
contradiction
by A2, Th62;
verum
end;
thus
t <> {}
by A2; verum