let X be set ; :: thesis:
let B be SetSequence of X; :: thesis:
let n be Nat; :: thesis:
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;

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

let Z be set ; :: thesis:
assume Z in { (B . k1) where k1 is Nat : n <= k1 } ; :: thesis:
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;

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

end;

hence x in Z by A8; :: thesis:

end;

end;

end;