let X be set ; :: thesis: for B being SetSequence of X

for n being Nat st B is V55() holds

(inferior_setsequence B) . (n + 1) c= B . n

let B be SetSequence of X; :: thesis: for n being Nat st B is V55() holds

(inferior_setsequence B) . (n + 1) c= B . n

let n be Nat; :: thesis: ( B is V55() implies (inferior_setsequence B) . (n + 1) c= B . n )

set Y = { (B . k) where k is Nat : n + 1 <= k } ;

assume B is V55() ; :: thesis: (inferior_setsequence B) . (n + 1) c= B . n

then A1: B . (n + 1) c= B . n by PROB_2:6;

A2: B . (n + 1) in { (B . k) where k is Nat : n + 1 <= k } ;

hence (inferior_setsequence B) . (n + 1) c= B . n by A3; :: thesis: verum

for n being Nat st B is V55() holds

(inferior_setsequence B) . (n + 1) c= B . n

let B be SetSequence of X; :: thesis: for n being Nat st B is V55() holds

(inferior_setsequence B) . (n + 1) c= B . n

let n be Nat; :: thesis: ( B is V55() implies (inferior_setsequence B) . (n + 1) c= B . n )

set Y = { (B . k) where k is Nat : n + 1 <= k } ;

assume B is V55() ; :: thesis: (inferior_setsequence B) . (n + 1) c= B . n

then A1: B . (n + 1) c= B . n by PROB_2:6;

A2: B . (n + 1) in { (B . k) where k is Nat : n + 1 <= k } ;

A3: now :: thesis: for x being object st x in meet { (B . k) where k is Nat : n + 1 <= k } holds

x in B . n

(inferior_setsequence B) . (n + 1) = meet { (B . k) where k is Nat : n + 1 <= k }
by Def2;x in B . n

let x be object ; :: thesis: ( x in meet { (B . k) where k is Nat : n + 1 <= k } implies x in B . n )

assume x in meet { (B . k) where k is Nat : n + 1 <= k } ; :: thesis: x in B . n

then x in B . (n + 1) by A2, SETFAM_1:def 1;

hence x in B . n by A1; :: thesis: verum

end;assume x in meet { (B . k) where k is Nat : n + 1 <= k } ; :: thesis: x in B . n

then x in B . (n + 1) by A2, SETFAM_1:def 1;

hence x in B . n by A1; :: thesis: verum

hence (inferior_setsequence B) . (n + 1) c= B . n by A3; :: thesis: verum