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

now

let n be Element of NAT ; :: thesis: (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n)
{ (B . k1) where k1 is Element of NAT : n <= k1 } = { (B . k2) where k2 is Element of NAT : n + 1 <= k2 } \/ {(B . n)} by Th2;
then union { (B . k2) where k2 is Element of NAT : n + 1 <= k2 } c= union { (B . k1) where k1 is Element of NAT : n <= k1 } by XBOOLE_1:7, ZFMISC_1:95;
then (superior_setsequence B) . (n + 1) c= union { (B . k1) where k1 is Element of NAT : n <= k1 } by Def3;
then A1: (superior_setsequence B) . (n + 1) c= (superior_setsequence B) . n by Def3;

A2: now

let x be set ; :: 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

proof

now

per cases ( x in (superior_setsequence B) . (n + 1) or x in B . n ) by A3;

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

hence x in (superior_setsequence B) . n by A1; :: thesis: verum

end;

case A4: x in B . n ; :: thesis: x in (superior_setsequence B) . n

B . n in { (B . k1) where k1 is Element of NAT : n <= k1 } ;
then x in union { (B . k1) where k1 is Element of NAT : n <= k1 } by A4, TARSKI:def 4;
hence x in (superior_setsequence B) . n by Def3; :: thesis: verum

end;

end;

end;

hence x in (superior_setsequence B) . n ; :: thesis: verum

end;

end;

now

let x be set ; :: 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 Element of NAT : n <= k1 } by Def3;
then consider Y1 being set such that
A5: ( x in Y1 & Y1 in { (B . k1) where k1 is Element of NAT : n <= k1 } ) by TARSKI:def 4;
consider k11 being Element of NAT such that
A6: ( Y1 = B . k11 & n <= k11 ) by A5;

now

per cases ( ( Y1 = B . k11 & n = k11 ) or ( Y1 = B . k11 & n + 1 <= k11 ) ) by A6, Lm1;

case ( Y1 = B . k11 & n = k11 ) ; :: thesis: x in B . n

hence x in B . n by A5; :: thesis: verum

end;

case ( Y1 = B . k11 & n + 1 <= k11 ) ; :: thesis: x in union { (B . k2) where k2 is Element of NAT : n + 1 <= k2 }

then Y1 in { (B . k2) where k2 is Element of NAT : n + 1 <= k2 } ;
hence x in union { (B . k2) where k2 is Element of NAT : n + 1 <= k2 } by A5, TARSKI:def 4; :: thesis: verum

end;

end;

end;

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

end;

then for x being set holds
( 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

end;

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