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 :: thesis: for G being set st G <> {} & G c= F & G is finite holds
meet G <> {}

defpred S₁[ object , object ] 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 object st x in G holds
ex y being object st
( y in NAT & S₁[x,y] )

proof

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

end;

consider f being Function of G,NAT such that
A8: for x being object 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:56;
A10: i in NAT by ORDINAL1:def 12;
dom S = NAT by FUNCT_2:def 1;
then S . i <> {} by A10, FUNCT_1:def 9;
then consider x being object such that
A11: x in S . i by XBOOLE_0:def 1;
A12: dom f = G by FUNCT_2:def 1;

now :: thesis: for Y being set st Y in G holds
x in Y

let Y be set ; :: thesis: ( Y in G implies x in Y )
assume A13: Y in G ; :: thesis: x in Y
then A14: f . Y in rng f by A12, FUNCT_1:def 3;
reconsider fY = f . Y as Nat ;
A15: fY <= i by A9, A14;
Y = S . fY by A8, A13;
then S . i c= Y by A1, A15, PROB_1:def 4;
hence x in Y by A11; :: 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:42;
hence F is centered by A3, FINSET_1:def 3; :: thesis: verum