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;

then A10: (inferior_setsequence B) . n c= (inferior_setsequence B) . (n + 1) by A1, A3, A2, SETFAM_1:6, XBOOLE_1:7;

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

{ (B . k2) where k2 is Nat : n + 1 <= k2 } <> {}
by Th1;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

hence x in (inferior_setsequence B) . n by Def2; :: thesis: verum

end;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

then
x in meet { (B . k2) where k2 is Nat : n <= k2 }
by A4, SETFAM_1:def 1;
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;

end;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 Z1end;

hence
x in Z
by A8; :: thesis: verumhence x in (inferior_setsequence B) . n by Def2; :: thesis: verum

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 )

hence
(inferior_setsequence B) . n = ((inferior_setsequence B) . (n + 1)) /\ (B . n)
by A5, XBOOLE_0:def 4; :: thesis: verum( 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;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