A1: for n being Nat holds (superior_setsequence B) . n = union { (B . k) where k is Nat : n <= k } by Def3;
dom (superior_setsequence B) = NAT by Def3;
hence superior_setsequence B is SetSequence of X by A1, Th16; :: thesis: verum