let I be 1 -element set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I
for P being Subset of (product (Carrier J)) holds
( P in FinMeetCl (product_prebasis J) iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )
let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: for i being Element of I
for P being Subset of (product (Carrier J)) holds
( P in FinMeetCl (product_prebasis J) iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )
let i be Element of I; :: thesis: for P being Subset of (product (Carrier J)) holds
( P in FinMeetCl (product_prebasis J) iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )
let P be Subset of (product (Carrier J)); :: thesis: ( P in FinMeetCl (product_prebasis J) iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )
thus ( P in FinMeetCl (product_prebasis J) implies ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) ) by Lm4; :: thesis: ( ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) implies P in FinMeetCl (product_prebasis J) )
given V being Subset of (J . i) such that A2: ( V is open & P = product ({i} --> V) ) ; :: thesis: P in FinMeetCl (product_prebasis J)
P in product_prebasis J by A2, Th64;
hence P in FinMeetCl (product_prebasis J) by TARSKI:def 3, CANTOR_1:4; :: thesis: verum