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

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