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

proof

let x be object ; :: thesis: ( x in UniCl (FinMeetCl (product_prebasis J)) iff x in product_prebasis J )
set i = the Element of I;

hereby :: thesis: ( x in product_prebasis J implies x in UniCl (FinMeetCl (product_prebasis J)) )

assume A1: x in UniCl (FinMeetCl (product_prebasis J)) ; :: thesis: x in product_prebasis J
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: verum

end;

assume A2: x in product_prebasis J ; :: thesis: x in UniCl (FinMeetCl (product_prebasis J))
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: verum

end;

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