let I be 1 -element set ; :: thesis:
let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis:
for x being object holds
( x in UniCl (FinMeetCl (product_prebasis J)) iff x in product_prebasis J )

proof

let x be object ; :: thesis:
set i = the Element of I;

hereby :: thesis:

assume A1: x in UniCl (FinMeetCl (product_prebasis J)) ; :: thesis:
then reconsider P = x as Subset of (product (Carrier J)) ;
ex V being Subset of (J . the Element of I) st
( V is open & P = product ({ the Element of I} --> V) ) by A1, Lm6;
hence x in product_prebasis J by Th64; :: thesis:

end;

assume A2: x in product_prebasis J ; :: thesis:
then reconsider P = x as Subset of (product (Carrier J)) ;
ex V being Subset of (J . the Element of I) st
( V is open & P = product ({ the Element of I} --> V) ) by A2, Th64;
hence x in UniCl (FinMeetCl (product_prebasis J)) by Lm6; :: thesis:

end;

hence UniCl (FinMeetCl (product_prebasis J)) = product_prebasis J by TARSKI:2; :: thesis: