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
dom S = NAT by FUNCT_2:def 1;
then A3: F <> {} by A2, RELAT_1:65;

now

let G be set ; :: thesis: ( G <> {} & G c= F & G is finite implies meet G <> {} )
assume A4: ( G <> {} & G c= F & G is finite ) ; :: thesis: meet G <> {}
defpred S₁[ set , set ] means $1 = S . $2;
A5: 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 A6: x in G ; :: thesis: ex y being set st
( y in NAT & S₁[x,y] )
ex y being set st
( y in dom S & S . y = x ) by A2, A4, A6, 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
A7: for x being set st x in G holds
S₁[x,f . x] from FUNCT_2:sch 1(A5);
A8: dom f = G by FUNCT_2:def 1;
consider i being Element of NAT such that
A9: for j being Element of NAT st j in rng f holds
j <= i by STIRL2_1:66, A4;
dom S = NAT by FUNCT_2:def 1;
then S . i <> {} by FUNCT_1:def 15;
then consider x being set such that
A10: x in S . i by XBOOLE_0:def 1;

now

let Y be set ; :: thesis: ( Y in G implies x in Y )
assume A11: Y in G ; :: thesis: x in Y
then A12: f . Y in rng f by A8, FUNCT_1:def 5;
then reconsider fY = f . Y as Element of NAT ;
( Y = S . fY & fY <= i ) by A7, A9, A11, A12;
then S . i c= Y by A1, 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;

hence F is centered by A3, FINSET_1:def 3; :: thesis: verum