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;
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
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
proof
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 ) )
per cases ( x in (superior_setsequence B) . (n + 1) or x in B . n ) by A3;
case A4: x in B . n ; :: thesis: x in (superior_setsequence B) . n
B . n in { (B . k1) where k1 is Nat : n <= k1 } ;
then x in union { (B . k1) where k1 is 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 :: 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) )
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;
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 } ) )
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 Nat : n + 1 <= k2 }
then Y1 in { (B . k2) where k2 is Nat : n + 1 <= k2 } ;
hence x in union { (B . k2) where k2 is 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 object 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