let T be non empty TopSpace; :: thesis: for S being non-empty SetSequence of T st S is non-ascending holds
for F being Subset-Family of T st F = rng S holds
F is centered
let S be non-empty SetSequence of T; :: thesis: ( S is non-ascending implies for F being Subset-Family of T st F = rng S holds
F is centered )
assume A1: S is non-ascending ; :: thesis: for F being Subset-Family of T st F = rng S holds
F is centered
let F be Subset-Family of T; :: thesis: ( F = rng S implies F is centered )
assume A2: F = rng S ; :: thesis: F is centered

A3: now

defpred S₁[ set , set ] means $1 = S . $2;
let G be set ; :: thesis: ( G <> {} & G c= F & G is finite implies meet G <> {} )
assume that
A4: G <> {} and
A5: G c= F and
A6: G is finite ; :: thesis: meet G <> {}
A7: for x being set st x in G holds
ex y being set st
( y in NAT & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in G implies ex y being set st
( y in NAT & S₁[x,y] ) )
assume x in G ; :: thesis: ex y being set st
( y in NAT & S₁[x,y] )
then ex y being set st
( y in dom S & S . y = x ) by A2, A5, FUNCT_1:def 5;
hence ex y being set st
( y in NAT & S₁[x,y] ) ; :: thesis: verum

end;

consider f being Function of G,NAT such that
A8: for x being set st x in G holds
S₁[x,f . x] from FUNCT_2:sch 1(A7);
consider i being Nat such that
A9: for j being Nat st j in rng f holds
j <= i by A6, STIRL2_1:66;
A: i in NAT by ORDINAL1:def 13;
dom S = NAT by FUNCT_2:def 1;
then S . i <> {} by A, FUNCT_1:def 15;
then consider x being set such that
A10: x in S . i by XBOOLE_0:def 1;
A11: dom f = G by FUNCT_2:def 1;

now

let Y be set ; :: thesis: ( Y in G implies x in Y )
assume A12: Y in G ; :: thesis: x in Y
then A13: f . Y in rng f by A11, FUNCT_1:def 5;
then reconsider fY = f . Y as Element of NAT ;
A14: fY <= i by A9, A13;
Y = S . fY by A8, A12;
then S . i c= Y by A, A1, A14, PROB_1:def 6;
hence x in Y by A10; :: thesis: verum

end;

hence meet G <> {} by A4, SETFAM_1:def 1; :: thesis: verum

end;

dom S = NAT by FUNCT_2:def 1;
then F <> {} by A2, RELAT_1:65;
hence F is centered by A3, FINSET_1:def 3; :: thesis: verum