let b1, b2, a be natural number ; :: thesis: ( b1 <= b2 iff seq a,b1 c= seq a,b2 )
thus ( b1 <= b2 implies seq a,b1 c= seq a,b2 ) :: thesis: ( seq a,b1 c= seq a,b2 implies b1 <= b2 )

proof

assume A1: b1 <= b2 ; :: thesis: seq a,b1 c= seq a,b2
let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in seq a,b1 or b in seq a,b2 )
assume A2: b in seq a,b1 ; :: thesis: b in seq a,b2
reconsider c = b as Element of NAT by A2;
A3: ( 1 + a <= c & c <= b1 + a ) by A2, Th1;
b1 + a <= b2 + a by A1, XREAL_1:8;
then c <= b2 + a by A3, XXREAL_0:2;
hence b in seq a,b2 by A3; :: thesis: verum

end;

assume A4: seq a,b1 c= seq a,b2 ; :: thesis: b1 <= b2

now

assume b1 <> 0 ; :: thesis: b1 <= b2
then b1 + a in seq a,b1 by Th3;
then b1 + a <= b2 + a by A4, Th1;
hence b1 <= b2 by XREAL_1:8; :: thesis: verum

end;

hence b1 <= b2 ; :: thesis: verum