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 ()) holds
( P in FinMeetCl () 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 ()) holds
( P in FinMeetCl () 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 ()) holds
( P in FinMeetCl () iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )

let P be Subset of (product ()); :: thesis: ( P in FinMeetCl () iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )

thus ( P in FinMeetCl () 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 () )

given V being Subset of (J . i) such that A2: ( V is open & P = product ({i} --> V) ) ; :: thesis:
P in product_prebasis J by ;
hence P in FinMeetCl () by ; :: thesis: verum