let X be set ; :: thesis: for B being SetSequence of X
for n being Nat st B is non-descending holds
B . n c= (superior_setsequence B) . (n + 1)
let B be SetSequence of X; :: thesis: for n being Nat st B is non-descending holds
B . n c= (superior_setsequence B) . (n + 1)
let n be Nat; :: thesis: ( B is non-descending implies B . n c= (superior_setsequence B) . (n + 1) )
assume B is non-descending ; :: thesis: B . n c= (superior_setsequence B) . (n + 1)
then A1: B . n c= B . (n + 1) by PROB_2:7;
B . n c= union { (B . k) where k is Nat : n + 1 <= k }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B . n or x in union { (B . k) where k is Nat : n + 1 <= k } )
A2: B . (n + 1) in { (B . k) where k is Nat : n + 1 <= k } ;
assume x in B . n ; :: thesis: x in union { (B . k) where k is Nat : n + 1 <= k }
hence x in union { (B . k) where k is Nat : n + 1 <= k } by A1, A2, TARSKI:def 4; :: thesis: verum

end;

hence B . n c= (superior_setsequence B) . (n + 1) by Def3; :: thesis: verum