let X be set ; :: thesis: for A being Subset of X

for B being SetSequence of X st B is constant & the_value_of B = A holds

for n being Nat holds (inferior_setsequence B) . n = A

let A be Subset of X; :: thesis: for B being SetSequence of X st B is constant & the_value_of B = A holds

for n being Nat holds (inferior_setsequence B) . n = A

let B be SetSequence of X; :: thesis: ( B is constant & the_value_of B = A implies for n being Nat holds (inferior_setsequence B) . n = A )

assume A1: ( B is constant & the_value_of B = A ) ; :: thesis: for n being Nat holds (inferior_setsequence B) . n = A

let n be Nat; :: thesis: (inferior_setsequence B) . n = A

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

hence (inferior_setsequence B) . n = A by A1, Th14; :: thesis: verum

for B being SetSequence of X st B is constant & the_value_of B = A holds

for n being Nat holds (inferior_setsequence B) . n = A

let A be Subset of X; :: thesis: for B being SetSequence of X st B is constant & the_value_of B = A holds

for n being Nat holds (inferior_setsequence B) . n = A

let B be SetSequence of X; :: thesis: ( B is constant & the_value_of B = A implies for n being Nat holds (inferior_setsequence B) . n = A )

assume A1: ( B is constant & the_value_of B = A ) ; :: thesis: for n being Nat holds (inferior_setsequence B) . n = A

let n be Nat; :: thesis: (inferior_setsequence B) . n = A

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

hence (inferior_setsequence B) . n = A by A1, Th14; :: thesis: verum