let A be Subset of RAT+ ; :: thesis: ( 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 <> {} ; :: thesis: ( 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 ; :: thesis: 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 Th66;
take {} ; :: thesis: ex r2, r3 being Element of RAT+ st
( {} in A & r2 in A & r3 in A & {} <> r2 & r2 <> r3 & r3 <> {} )
take x ; :: thesis: ex r3 being Element of RAT+ st
( {} in A & x in A & r3 in A & {} <> x & x <> r3 & r3 <> {} )
take t ; :: thesis: ( {} in A & x in A & t in A & {} <> x & x <> t & t <> {} )
x <=' t by A4, Def13;
hence ( {} in A & x in A & t in A ) by A1, A3, Th71; :: thesis: ( {} <> x & x <> t & t <> {} )
thus {} <> x by A2, A4, Th56; :: thesis: ( x <> t & t <> {} )

hereby :: thesis: t <> {}

assume x = t ; :: thesis: contradiction
then t + {} = t + t by A4, Th56;
hence contradiction by A2, Th69; :: thesis: verum

end;

thus t <> {} by A2; :: thesis: verum