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 )
proof
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;
assume A4: seq (a,b1) c= seq (a,b2) ; :: thesis: b1 <= b2
now :: thesis: ( b1 <> 0 implies b1 <= b2 )
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:6; :: thesis: verum
end;
hence b1 <= b2 ; :: thesis: verum