for n being Nat holds (superior_setsequence A) . n = union { (A . k) where k is Nat : n <= k } by SETLIM_1:def 3;
hence superior_setsequence A is SetSequence of X ; :: thesis: verum