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 & 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 A2: 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
A3: 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 <> {} )
( {} <=' t & x <=' t ) by A3, Def13, Th71;
hence ( {} in A & x in A & t in A ) by A1, A2; :: thesis: ( {} <> x & x <> t & t <> {} )
thus {} <> x by A1, A3, Th56; :: thesis: ( x <> t & t <> {} )

hereby :: thesis: t <> {}

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

end;

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