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

now

let n be Element of NAT ; :: thesis: (inferior_setsequence B) . n = ((inferior_setsequence B) . (n + 1)) /\ (B . n)
A0: (inferior_setsequence B) . n = meet { (B . k1) where k1 is Element of NAT : n <= k1 } by def2;
B: (inferior_setsequence B) . (n + 1) = meet { (B . k2) where k2 is Element of NAT : n + 1 <= k2 } by def2;
AB0: { (B . k1) where k1 is Element of NAT : n <= k1 } <> {} by Th5;
AB1: { (B . k2) where k2 is Element of NAT : n + 1 <= k2 } <> {} by Th5;
{ (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 A2: (inferior_setsequence B) . n c= (inferior_setsequence B) . (n + 1) by A0, B, AB1, SETFAM_1:7, XBOOLE_1:7;

A3: now

let x be set ; :: thesis: ( x in (inferior_setsequence B) . n implies ( x in (inferior_setsequence B) . (n + 1) & x in B . n ) )
assume AA0: x in (inferior_setsequence B) . n ; :: thesis: ( x in (inferior_setsequence B) . (n + 1) & x in B . n )
B . n in { (B . k1) where k1 is Element of NAT : n <= k1 } ;
hence ( x in (inferior_setsequence B) . (n + 1) & x in B . n ) by A0, AA0, A2, SETFAM_1:def 1; :: thesis: verum

end;

A4: now

let x be set ; :: thesis: ( x in (inferior_setsequence B) . (n + 1) & x in B . n implies x in (inferior_setsequence B) . n )
assume BB0: ( x in (inferior_setsequence B) . (n + 1) & x in B . n ) ; :: thesis: x in (inferior_setsequence B) . n
for Z being set st Z in { (B . k2) where k2 is Element of NAT : n <= k2 } holds
x in Z

proof

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

now

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

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

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

end;

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

then Z1 in { (B . k2) where k2 is Element of NAT : n + 1 <= k2 } ;
hence x in Z1 by B, BB0, SETFAM_1:def 1; :: thesis: verum

end;

end;

end;

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

end;

then x in meet { (B . k2) where k2 is Element of NAT : n <= k2 } by AB0, SETFAM_1:def 1;
hence x in (inferior_setsequence B) . n by def2; :: thesis: verum

end;

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

end;

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