let n be Nat; :: thesis: for X being set

for B being SetSequence of X st B is V56() holds

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

let X be set ; :: thesis: for B being SetSequence of X st B is V56() holds

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

let B be SetSequence of X; :: thesis: ( B is V56() implies B . n c= (inferior_setsequence B) . (n + 1) )

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

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

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B . n or x in (inferior_setsequence B) . (n + 1) )

assume A2: x in B . n ; :: thesis: x in (inferior_setsequence B) . (n + 1)

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

hence x in (inferior_setsequence B) . (n + 1) by A6, A3, SETFAM_1:def 1; :: thesis: verum

for B being SetSequence of X st B is V56() holds

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

let X be set ; :: thesis: for B being SetSequence of X st B is V56() holds

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

let B be SetSequence of X; :: thesis: ( B is V56() implies B . n c= (inferior_setsequence B) . (n + 1) )

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

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

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B . n or x in (inferior_setsequence B) . (n + 1) )

assume A2: x in B . n ; :: thesis: x in (inferior_setsequence B) . (n + 1)

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

x in y

A6:
{ (B . k) where k is Nat : n + 1 <= k } <> {}
by Th1;x in y

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

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

then consider k1 being Nat such that

A4: y = B . k1 and

A5: n + 1 <= k1 ;

n <= k1 by A5, NAT_1:13;

then B . n c= B . k1 by A1, PROB_1:def 5;

hence x in y by A2, A4; :: thesis: verum

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

then consider k1 being Nat such that

A4: y = B . k1 and

A5: n + 1 <= k1 ;

n <= k1 by A5, NAT_1:13;

then B . n c= B . k1 by A1, PROB_1:def 5;

hence x in y by A2, A4; :: thesis: verum

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

hence x in (inferior_setsequence B) . (n + 1) by A6, A3, SETFAM_1:def 1; :: thesis: verum