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 )

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

hence
UniCl (FinMeetCl (product_prebasis J)) = product_prebasis J
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in UniCl (FinMeetCl (product_prebasis J)) iff x in product_prebasis J )

set i = the Element of I;

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;set i = the Element of I;

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

assume A2:
x in product_prebasis J
; :: thesis: 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;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

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