let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I
for P being non empty Subset of (product ()) st P in FinMeetCl () holds
ex I0 being finite Subset of I st
for i being Element of I holds
( (proj (J,i)) .: P is open & ( not i in I0 implies (proj (J,i)) .: P = [#] (J . i) ) )

let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: for P being non empty Subset of (product ()) st P in FinMeetCl () holds
ex I0 being finite Subset of I st
for i being Element of I holds
( (proj (J,i)) .: P is open & ( not i in I0 implies (proj (J,i)) .: P = [#] (J . i) ) )

let P be non empty Subset of (product ()); :: thesis: ( P in FinMeetCl () implies ex I0 being finite Subset of I st
for i being Element of I holds
( (proj (J,i)) .: P is open & ( not i in I0 implies (proj (J,i)) .: P = [#] (J . i) ) ) )

assume P in FinMeetCl () ; :: thesis: ex I0 being finite Subset of I st
for i being Element of I holds
( (proj (J,i)) .: P is open & ( not i in I0 implies (proj (J,i)) .: P = [#] (J . i) ) )

then consider X being Subset-Family of (product ()), f being I -valued one-to-one Function such that
A1: ( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X ) and
A2: for i being Element of I holds
( (proj (J,i)) .: P is open & ( not i in rng f implies (proj (J,i)) .: P = [#] (J . i) ) ) by Th62;
reconsider I0 = rng f as finite Subset of I by ;
take I0 ; :: thesis: for i being Element of I holds
( (proj (J,i)) .: P is open & ( not i in I0 implies (proj (J,i)) .: P = [#] (J . i) ) )

thus for i being Element of I holds
( (proj (J,i)) .: P is open & ( not i in I0 implies (proj (J,i)) .: P = [#] (J . i) ) ) by A2; :: thesis: verum