let X be set ; :: thesis: for B being SetSequence of X

for n being Nat st B is V56() holds

B . n c= (superior_setsequence B) . (n + 1)

let B be SetSequence of X; :: thesis: for n being Nat st B is V56() holds

B . n c= (superior_setsequence B) . (n + 1)

let n be Nat; :: thesis: ( B is V56() implies B . n c= (superior_setsequence B) . (n + 1) )

assume B is V56() ; :: 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 }

for n being Nat st B is V56() holds

B . n c= (superior_setsequence B) . (n + 1)

let B be SetSequence of X; :: thesis: for n being Nat st B is V56() holds

B . n c= (superior_setsequence B) . (n + 1)

let n be Nat; :: thesis: ( B is V56() implies B . n c= (superior_setsequence B) . (n + 1) )

assume B is V56() ; :: 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

hence
B . n c= (superior_setsequence B) . (n + 1)
by Def3; :: thesis: verum
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;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