let I be 2 -element set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I
for i, j being Element of I
for P being Subset of (product ()) st i <> j & P in FinMeetCl () holds
ex V being Subset of (J . i) ex W being Subset of (J . j) st
( V is open & W is open & P = product ((i,j) --> (V,W)) )

let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: for i, j being Element of I
for P being Subset of (product ()) st i <> j & P in FinMeetCl () holds
ex V being Subset of (J . i) ex W being Subset of (J . j) st
( V is open & W is open & P = product ((i,j) --> (V,W)) )

let i, j be Element of I; :: thesis: for P being Subset of (product ()) st i <> j & P in FinMeetCl () holds
ex V being Subset of (J . i) ex W being Subset of (J . j) st
( V is open & W is open & P = product ((i,j) --> (V,W)) )

let P be Subset of (product ()); :: thesis: ( i <> j & P in FinMeetCl () implies ex V being Subset of (J . i) ex W being Subset of (J . j) st
( V is open & W is open & P = product ((i,j) --> (V,W)) ) )

assume A1: ( i <> j & P in FinMeetCl () ) ; :: thesis: ex V being Subset of (J . i) ex W being Subset of (J . j) st
( V is open & W is open & P = product ((i,j) --> (V,W)) )

then consider X being Subset-Family of (product ()), f being I -valued one-to-one Function such that
A2: ( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X ) and
A3: P = product (() +* ()) by Lm3;
set F = () +* ();
( i in I & j in I ) ;
then A4: ( i in dom () & j in dom () ) by PARTFUN1:def 2;
rng f c= I ;
then rng f c= {i,j} by ;
per cases then ( rng f = {} or rng f = {i} or rng f = {j} or rng f = {i,j} ) by ZFMISC_1:36;
suppose rng f = {} ; :: thesis: ex V being Subset of (J . i) ex W being Subset of (J . j) st
( V is open & W is open & P = product ((i,j) --> (V,W)) )

then product_basis_selector (J,f) = {} ;
then A5: P = product ((i,j) --> ((() . i),(() . j))) by A1, A3, Th9
.= product ((i,j) --> (([#] (J . i)),(() . j))) by PENCIL_3:7
.= product ((i,j) --> (([#] (J . i)),([#] (J . j)))) by PENCIL_3:7 ;
thus ex V being Subset of (J . i) ex W being Subset of (J . j) st
( V is open & W is open & P = product ((i,j) --> (V,W)) ) by A5; :: thesis: verum
end;
suppose A6: rng f = {i} ; :: thesis: ex V being Subset of (J . i) ex W being Subset of (J . j) st
( V is open & W is open & P = product ((i,j) --> (V,W)) )

then A7: dom f = {((f ") . i)} by Th1;
A8: i in rng f by ;
A9: (f ") . i in X by ;
then reconsider V0 = (f ") . i as Subset of (product ()) ;
reconsider V = (proj (J,i)) .: V0 as Subset of (J . i) ;
take V ; :: thesis: ex W being Subset of (J . j) st
( V is open & W is open & P = product ((i,j) --> (V,W)) )

take [#] (J . j) ; :: thesis: ( V is open & [#] (J . j) is open & P = product ((i,j) --> (V,([#] (J . j)))) )
( V0 is empty or not V0 is empty ) ;
hence ( V is open & [#] (J . j) is open ) by A2, A9, Th58; :: thesis: P = product ((i,j) --> (V,([#] (J . j))))
product_basis_selector (J,f) = {i} --> (() . i) by
.= {i} --> ((proj (J,i)) .: ((f ") . i)) by
.= i .--> V by FUNCOP_1:def 9 ;
then () +* () = () +* (i,V) by
.= (i,j) --> (V,(() . j)) by
.= (i,j) --> (V,([#] (J . j))) by PENCIL_3:7 ;
hence P = product ((i,j) --> (V,([#] (J . j)))) by A3; :: thesis: verum
end;
suppose A10: rng f = {j} ; :: thesis: ex V being Subset of (J . i) ex W being Subset of (J . j) st
( V is open & W is open & P = product ((i,j) --> (V,W)) )

then A11: dom f = {((f ") . j)} by Th1;
A12: j in rng f by ;
A13: (f ") . j in X by ;
then reconsider W0 = (f ") . j as Subset of (product ()) ;
reconsider W = (proj (J,j)) .: W0 as Subset of (J . j) ;
take [#] (J . i) ; :: thesis: ex W being Subset of (J . j) st
( [#] (J . i) is open & W is open & P = product ((i,j) --> (([#] (J . i)),W)) )

take W ; :: thesis: ( [#] (J . i) is open & W is open & P = product ((i,j) --> (([#] (J . i)),W)) )
thus [#] (J . i) is open ; :: thesis: ( W is open & P = product ((i,j) --> (([#] (J . i)),W)) )
( W0 is empty or not W0 is empty ) ;
hence W is open by ; :: thesis: P = product ((i,j) --> (([#] (J . i)),W))
product_basis_selector (J,f) = {j} --> (() . j) by
.= {j} --> ((proj (J,j)) .: ((f ") . j)) by
.= j .--> W by FUNCOP_1:def 9 ;
then () +* () = () +* (j,W) by
.= (i,j) --> ((() . i),W) by
.= (i,j) --> (([#] (J . i)),W) by PENCIL_3:7 ;
hence P = product ((i,j) --> (([#] (J . i)),W)) by A3; :: thesis: verum
end;
suppose A14: rng f = {i,j} ; :: thesis: ex V being Subset of (J . i) ex W being Subset of (J . j) st
( V is open & W is open & P = product ((i,j) --> (V,W)) )

then A15: dom f = {((f ") . i),((f ") . j)} by Th2;
A16: ( i in rng f & j in rng f ) by ;
A17: ( (f ") . i in X & (f ") . j in X ) by ;
then reconsider V0 = (f ") . i as Subset of (product ()) ;
reconsider V = (proj (J,i)) .: V0 as Subset of (J . i) ;
reconsider W0 = (f ") . j as Subset of (product ()) by A17;
reconsider W = (proj (J,j)) .: W0 as Subset of (J . j) ;
take V ; :: thesis: ex W being Subset of (J . j) st
( V is open & W is open & P = product ((i,j) --> (V,W)) )

take W ; :: thesis: ( V is open & W is open & P = product ((i,j) --> (V,W)) )
( V0 is empty or not V0 is empty ) ;
hence V is open by ; :: thesis: ( W is open & P = product ((i,j) --> (V,W)) )
( W0 is empty or not W0 is empty ) ;
hence W is open by ; :: thesis: P = product ((i,j) --> (V,W))
rng f = I by A1, A14, Th8;
then A18: product_basis_selector (J,f) = (i,j) --> ((() . i),(() . j)) by
.= (i,j) --> ((() . i),((proj (J,j)) .: ((f ") . j))) by
.= (i,j) --> (V,W) by ;
dom () = I by PARTFUN1:def 2
.= {i,j} by ;
then dom () = dom () by ;
hence P = product ((i,j) --> (V,W)) by ; :: thesis: verum
end;
end;