let Z be set ; :: thesis: ( Z in { (B . k2) where k2 is Nat : n <= k2 } implies x in Z ) assume
Z in { (B . k1) where k1 is Nat : n <= k1 }
; :: thesis: x in Z then consider Z1 being set such that A8:
( Z = Z1 & Z1 in { (B . k1) where k1 is Nat : n <= k1 } )
; consider k11 being Nat such that A9:
( Z1 = B . k11 & n <= k11 )
byA8;