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

dom (superior_setsequence B) = NAT by Def3;

hence superior_setsequence B is SetSequence of X by A1, Th16; :: thesis: verum