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