for a, b1, b2 being Nat holds
( b1 <= b2 iff seq (a,b1) c= seq (a,b2) )