let X be set ; :: thesis: for B being SetSequence of X holds inferior_setsequence B is V50()
let B be SetSequence of X; :: thesis: inferior_setsequence B is V50()

now :: thesis: for n being Element of NAT holds (inferior_setsequence B) . n c= (inferior_setsequence B) . (n + 1)

let n be Element of NAT ; :: thesis: (inferior_setsequence B) . n c= (inferior_setsequence B) . (n + 1)
(inferior_setsequence B) . n = ((inferior_setsequence B) . (n + 1)) /\ (B . n) by Th21;
hence (inferior_setsequence B) . n c= (inferior_setsequence B) . (n + 1) by XBOOLE_1:17; :: thesis: verum

end;

hence inferior_setsequence B is V50() by PROB_2:7; :: thesis: verum