let T be non empty TopSpace; :: thesis:
let S be non-empty SetSequence of T; :: thesis:
assume A1: S is V176() ; :: thesis:
let F be Subset-Family of T; :: thesis:
assume A2: F = rng S ; :: thesis:

A3: now :: thesis:

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

let x be object ; :: thesis:
assume x in G ; :: thesis:
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:

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;

let Y be set ; :: thesis:
assume A13: Y in G ; :: thesis:
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:

end;

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

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: