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

for n being Nat holds (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n)

let B be SetSequence of X; :: thesis: for n being Nat holds (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n)

let n be Nat; :: thesis: (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n)

{ (B . k1) where k1 is Nat : n <= k1 } = { (B . k2) where k2 is Nat : n + 1 <= k2 } \/ {(B . n)} by Th2;

then union { (B . k2) where k2 is Nat : n + 1 <= k2 } c= union { (B . k1) where k1 is Nat : n <= k1 } by XBOOLE_1:7, ZFMISC_1:77;

then (superior_setsequence B) . (n + 1) c= union { (B . k1) where k1 is Nat : n <= k1 } by Def3;

then A1: (superior_setsequence B) . (n + 1) c= (superior_setsequence B) . n by Def3;

( x in (superior_setsequence B) . n iff ( x in B . n or x in (superior_setsequence B) . (n + 1) ) ) by A2;

hence (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n) by XBOOLE_0:def 3; :: thesis: verum

for n being Nat holds (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n)

let B be SetSequence of X; :: thesis: for n being Nat holds (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n)

let n be Nat; :: thesis: (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n)

{ (B . k1) where k1 is Nat : n <= k1 } = { (B . k2) where k2 is Nat : n + 1 <= k2 } \/ {(B . n)} by Th2;

then union { (B . k2) where k2 is Nat : n + 1 <= k2 } c= union { (B . k1) where k1 is Nat : n <= k1 } by XBOOLE_1:7, ZFMISC_1:77;

then (superior_setsequence B) . (n + 1) c= union { (B . k1) where k1 is Nat : n <= k1 } by Def3;

then A1: (superior_setsequence B) . (n + 1) c= (superior_setsequence B) . n by Def3;

A2: now :: thesis: for x being object st ( x in (superior_setsequence B) . (n + 1) or x in B . n ) holds

x in (superior_setsequence B) . n

x in (superior_setsequence B) . n

let x be object ; :: thesis: ( ( x in (superior_setsequence B) . (n + 1) or x in B . n ) implies x in (superior_setsequence B) . n )

assume A3: ( x in (superior_setsequence B) . (n + 1) or x in B . n ) ; :: thesis: x in (superior_setsequence B) . n

thus x in (superior_setsequence B) . n :: thesis: verum

end;assume A3: ( x in (superior_setsequence B) . (n + 1) or x in B . n ) ; :: thesis: x in (superior_setsequence B) . n

thus x in (superior_setsequence B) . n :: thesis: verum

proof

end;

now :: thesis: ( ( x in (superior_setsequence B) . (n + 1) & x in (superior_setsequence B) . n ) or ( x in B . n & x in (superior_setsequence B) . n ) )end;

hence
x in (superior_setsequence B) . n
; :: thesis: verumper cases
( x in (superior_setsequence B) . (n + 1) or x in B . n )
by A3;

end;

now :: thesis: for x being object holds

( not x in (superior_setsequence B) . n or x in B . n or x in (superior_setsequence B) . (n + 1) )

then
for x being object holds ( not x in (superior_setsequence B) . n or x in B . n or x in (superior_setsequence B) . (n + 1) )

let x be object ; :: thesis: ( not x in (superior_setsequence B) . n or x in B . n or x in (superior_setsequence B) . (n + 1) )

assume x in (superior_setsequence B) . n ; :: thesis: ( x in B . n or x in (superior_setsequence B) . (n + 1) )

then x in union { (B . k1) where k1 is Nat : n <= k1 } by Def3;

then consider Y1 being set such that

A5: ( x in Y1 & Y1 in { (B . k1) where k1 is Nat : n <= k1 } ) by TARSKI:def 4;

consider k11 being Nat such that

A6: ( Y1 = B . k11 & n <= k11 ) by A5;

end;assume x in (superior_setsequence B) . n ; :: thesis: ( x in B . n or x in (superior_setsequence B) . (n + 1) )

then x in union { (B . k1) where k1 is Nat : n <= k1 } by Def3;

then consider Y1 being set such that

A5: ( x in Y1 & Y1 in { (B . k1) where k1 is Nat : n <= k1 } ) by TARSKI:def 4;

consider k11 being Nat such that

A6: ( Y1 = B . k11 & n <= k11 ) by A5;

now :: thesis: ( ( Y1 = B . k11 & n = k11 & x in B . n ) or ( Y1 = B . k11 & n + 1 <= k11 & x in union { (B . k2) where k2 is Nat : n + 1 <= k2 } ) )end;

hence
( x in B . n or x in (superior_setsequence B) . (n + 1) )
by Def3; :: thesis: verum( x in (superior_setsequence B) . n iff ( x in B . n or x in (superior_setsequence B) . (n + 1) ) ) by A2;

hence (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n) by XBOOLE_0:def 3; :: thesis: verum