let X be set ; :: thesis: for B being SetSequence of X
for n being Nat holds (inferior_setsequence B) . n = ((inferior_setsequence B) . (n + 1)) /\ (B . n)
let B be SetSequence of X; :: thesis: for n being Nat holds (inferior_setsequence B) . n = ((inferior_setsequence B) . (n + 1)) /\ (B . n)
let n be Nat; :: thesis: (inferior_setsequence B) . n = ((inferior_setsequence B) . (n + 1)) /\ (B . n)
A1: (inferior_setsequence B) . n = meet { (B . k1) where k1 is Nat : n <= k1 } by Def2;
A2: { (B . k1) where k1 is Nat : n <= k1 } = { (B . k2) where k2 is Nat : n + 1 <= k2 } \/ {(B . n)} by Th2;
A3: (inferior_setsequence B) . (n + 1) = meet { (B . k2) where k2 is Nat : n + 1 <= k2 } by Def2;
A4: { (B . k1) where k1 is Nat : n <= k1 } <> {} by Th1;

A5: now :: thesis: for x being object st x in (inferior_setsequence B) . (n + 1) & x in B . n holds
x in (inferior_setsequence B) . n

let x be object ; :: thesis: ( x in (inferior_setsequence B) . (n + 1) & x in B . n implies x in (inferior_setsequence B) . n )
assume that
A6: x in (inferior_setsequence B) . (n + 1) and
A7: x in B . n ; :: thesis: x in (inferior_setsequence B) . n
for Z being set st Z in { (B . k2) where k2 is Nat : n <= k2 } holds
x in Z

proof

let Z be set ; :: thesis: ( Z in { (B . k2) where k2 is Nat : n <= k2 } implies x in Z )
assume Z in { (B . k1) where k1 is Nat : n <= k1 } ; :: thesis: x in Z
then consider Z1 being set such that
A8: ( Z = Z1 & Z1 in { (B . k1) where k1 is Nat : n <= k1 } ) ;
consider k11 being Nat such that
A9: ( Z1 = B . k11 & n <= k11 ) by A8;

now :: thesis: x in Z1

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

suppose ( Z1 = B . k11 & n = k11 ) ; :: thesis: x in Z1

hence x in Z1 by A7; :: thesis: verum

end;

suppose ( Z1 = B . k11 & n + 1 <= k11 ) ; :: thesis: x in Z1

then Z1 in { (B . k2) where k2 is Nat : n + 1 <= k2 } ;
hence x in Z1 by A3, A6, SETFAM_1:def 1; :: thesis: verum

end;

end;

end;

hence x in Z by A8; :: thesis: verum

end;

then x in meet { (B . k2) where k2 is Nat : n <= k2 } by A4, SETFAM_1:def 1;
hence x in (inferior_setsequence B) . n by Def2; :: thesis: verum

end;

{ (B . k2) where k2 is Nat : n + 1 <= k2 } <> {} by Th1;
then A10: (inferior_setsequence B) . n c= (inferior_setsequence B) . (n + 1) by A1, A3, A2, SETFAM_1:6, XBOOLE_1:7;

now :: thesis: for x being object st x in (inferior_setsequence B) . n holds
( x in (inferior_setsequence B) . (n + 1) & x in B . n )

let x be object ; :: thesis: ( x in (inferior_setsequence B) . n implies ( x in (inferior_setsequence B) . (n + 1) & x in B . n ) )
A11: B . n in { (B . k1) where k1 is Nat : n <= k1 } ;
assume x in (inferior_setsequence B) . n ; :: thesis: ( x in (inferior_setsequence B) . (n + 1) & x in B . n )
hence ( x in (inferior_setsequence B) . (n + 1) & x in B . n ) by A1, A10, A11, SETFAM_1:def 1; :: thesis: verum

end;

hence (inferior_setsequence B) . n = ((inferior_setsequence B) . (n + 1)) /\ (B . n) by A5, XBOOLE_0:def 4; :: thesis: verum