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 b1 <= b2 ; :: thesis: seq a,b1 c= seq a,b2
then A1: b1 + a <= b2 + a by XREAL_1:8;
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;
c <= b1 + a by A2, Th1;
then A3: c <= b2 + a by A1, XXREAL_0:2;
1 + a <= c by A2, Th1;
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