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 Th6;
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 A2: (superior_setsequence B) . (n + 1) c= (superior_setsequence B) . n by def3;
A3: 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
AB: ( 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
AA2: ( Y1 = B . k11 & n <= k11 ) by AB;
now
per cases ( ( Y1 = B . k11 & n = k11 ) or ( Y1 = B . k11 & n + 1 <= k11 ) ) by AA2, LM1;
case ( Y1 = B . k11 & n = k11 ) ; :: thesis: x in B . n
hence x in B . n by AB; :: 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 AB, 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;
A4: 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 BB0: ( 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 BB0;
case CA2: 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 CA2, 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;
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 A3, A4;
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