let r, s, t be Element of RAT+ ; :: thesis: ( r <=' s *' t implies ex t0 being Element of RAT+ st
( r = s *' t0 & t0 <=' t ) )
given x being Element of RAT+ such that A1: s *' t = r + x ; :: according to ARYTM_3:def 13 :: thesis: ex t0 being Element of RAT+ st
( r = s *' t0 & t0 <=' t )

per cases ( s = {} or s <> {} ) ;

suppose A2: s = {} ; :: thesis: ex t0 being Element of RAT+ st
( r = s *' t0 & t0 <=' t )

take t ; :: thesis: ( r = s *' t & t <=' t )
s *' t = {} by A2, Th48;
hence ( r = s *' t & t <=' t ) by A1, Th63; :: thesis: verum

end;

suppose A3: s <> {} ; :: thesis: ex t0 being Element of RAT+ st
( r = s *' t0 & t0 <=' t )

then consider t1 being Element of RAT+ such that
A4: x = s *' t1 by Th55;
consider t0 being Element of RAT+ such that
A5: r = s *' t0 by A3, Th55;
take t0 ; :: thesis: ( r = s *' t0 & t0 <=' t )
thus r = s *' t0 by A5; :: thesis: t0 <=' t
take t1 ; :: according to ARYTM_3:def 13 :: thesis: t = t0 + t1
s *' t = s *' (t0 + t1) by A1, A5, A4, Th57;
hence t = t0 + t1 by A3, Th56; :: thesis: verum

end;

end;