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 Element of 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 Element of 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 Element of NAT holds (inferior_setsequence B) . n = A )
assume B: ( B is constant & the_value_of B = A ) ; :: thesis: for n being Element of NAT holds (inferior_setsequence B) . n = A
let n be Element of NAT ; :: thesis: (inferior_setsequence B) . n = A
(inferior_setsequence B) . n = meet { (B . k) where k is Element of NAT : n <= k } by def2;
hence (inferior_setsequence B) . n = A by B, Th191; :: thesis: verum