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

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

let n be Element of NAT ; :: thesis: (superior_setsequence B) . (n + 1) c= (superior_setsequence B) . n
(superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n) by Th22;
hence (superior_setsequence B) . (n + 1) c= (superior_setsequence B) . n by XBOOLE_1:7; :: thesis: verum

end;

hence superior_setsequence B is V49() by PROB_2:6; :: thesis: verum