let a, b1, b2 be Nat; :: 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 )

thus ( b1 <= b2 implies seq (a,b1) c= seq (a,b2) ) :: thesis: ( seq (a,b1) c= seq (a,b2) implies b1 <= b2 )

proof

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

then A1: b1 + a <= b2 + a by XREAL_1:6;

let b be object ; :: 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;then A1: b1 + a <= b2 + a by XREAL_1:6;

let b be object ; :: 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

now :: thesis: ( b1 <> 0 implies b1 <= b2 )

hence
b1 <= b2
; :: thesis: verumassume
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:6; :: thesis: verum

end;then b1 + a in seq (a,b1) by Th3;

then b1 + a <= b2 + a by A4, Th1;

hence b1 <= b2 by XREAL_1:6; :: thesis: verum