A1:
for n being Nat holds (inferior_setsequence B) . n = meet { (B . k) where k is Nat : n <= k }
by Def2;

dom (inferior_setsequence B) = NAT by Def2;

hence inferior_setsequence B is SetSequence of X by A1, Th15; :: thesis: verum

dom (inferior_setsequence B) = NAT by Def2;

hence inferior_setsequence B is SetSequence of X by A1, Th15; :: thesis: verum