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