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 X being Subset-Family of (product ()) ex f being I -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & ( 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) ) ) ) )

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 X being Subset-Family of (product ()) ex f being I -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & ( 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) ) ) ) )

let P be non empty Subset of (product ()); :: thesis: ( P in FinMeetCl () implies ex X being Subset-Family of (product ()) ex f being I -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & ( 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) ) ) ) ) )

assume A1: P in FinMeetCl () ; :: thesis: ex X being Subset-Family of (product ()) ex f being I -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & ( 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) ) ) ) )

consider X being Subset-Family of (product ()), f being I -valued one-to-one Function such that
A2: ( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X ) and
A3: P = product (() +* ()) by ;
take X ; :: thesis: ex f being I -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & ( 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) ) ) ) )

take f ; :: thesis: ( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & ( 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) ) ) ) )

thus ( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X ) by A2; :: thesis: 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) ) )

A4: now :: thesis: for A being Subset of (product ()) st A in X holds
(proj (J,(f /. A))) .: A is open
let A be Subset of (product ()); :: thesis: ( A in X implies (proj (J,(f /. A))) .: A is open )
assume A5: A in X ; :: thesis: (proj (J,(f /. A))) .: A is open
( A is empty implies (proj (J,(f /. A))) .: A = {} (J . (f /. A)) ) ;
hence (proj (J,(f /. A))) .: A is open by A2, A5, Th58; :: thesis: verum
end;
f " is non-empty
proof end;
hence 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 A2, A3, A4, Th60; :: thesis: verum