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 (Carrier J)) st i <> j & P in FinMeetCl (product_prebasis J) 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 (Carrier J)) st i <> j & P in FinMeetCl (product_prebasis J) 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 (Carrier J)) st i <> j & P in FinMeetCl (product_prebasis J) 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 (Carrier J)); :: thesis: ( i <> j & P in FinMeetCl (product_prebasis J) 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 (product_prebasis 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 consider X being Subset-Family of (product (Carrier J)), 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 ((Carrier J) +* (product_basis_selector (J,f))) by Lm3;
set F = (Carrier J) +* (product_basis_selector (J,f));
( i in I & j in I ) ;
then A4: ( i in dom (Carrier J) & j in dom (Carrier J) ) by PARTFUN1:def 2;
rng f c= I ;
then rng f c= {i,j} by A1, Th8;

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) --> (((Carrier J) . i),((Carrier J) . j))) by A1, A3, Th9
.= product ((i,j) --> (([#] (J . i)),((Carrier J) . 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 A6, TARSKI:def 1;
A9: (f ") . i in X by A2, A7, TARSKI:def 1;
then reconsider V0 = (f ") . i as Subset of (product (Carrier J)) ;
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} --> ((product_basis_selector (J,f)) . i) by A6, Th7
.= {i} --> ((proj (J,i)) .: ((f ") . i)) by A8, Th54
.= i .--> V by FUNCOP_1:def 9 ;
then (Carrier J) +* (product_basis_selector (J,f)) = (Carrier J) +* (i,V) by A4, FUNCT_7:def 3
.= (i,j) --> (V,((Carrier J) . j)) by A1, Th34
.= (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 A10, TARSKI:def 1;
A13: (f ") . j in X by A2, A11, TARSKI:def 1;
then reconsider W0 = (f ") . j as Subset of (product (Carrier J)) ;
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 A2, A13, Th58; :: thesis: P = product ((i,j) --> (([#] (J . i)),W))
product_basis_selector (J,f) = {j} --> ((product_basis_selector (J,f)) . j) by A10, Th7
.= {j} --> ((proj (J,j)) .: ((f ") . j)) by A12, Th54
.= j .--> W by FUNCOP_1:def 9 ;
then (Carrier J) +* (product_basis_selector (J,f)) = (Carrier J) +* (j,W) by A4, FUNCT_7:def 3
.= (i,j) --> (((Carrier J) . i),W) by A1, Th34
.= (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 A14, TARSKI:def 2;
A17: ( (f ") . i in X & (f ") . j in X ) by A2, A15, TARSKI:def 2;
then reconsider V0 = (f ") . i as Subset of (product (Carrier J)) ;
reconsider V = (proj (J,i)) .: V0 as Subset of (J . i) ;
reconsider W0 = (f ") . j as Subset of (product (Carrier J)) 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 A2, A17, Th58; :: thesis: ( W is open & P = product ((i,j) --> (V,W)) )
( W0 is empty or not W0 is empty ) ;
hence W is open by A2, A17, Th58; :: thesis: P = product ((i,j) --> (V,W))
rng f = I by A1, A14, Th8;
then A18: product_basis_selector (J,f) = (i,j) --> (((product_basis_selector (J,f)) . i),((product_basis_selector (J,f)) . j)) by A1, Th9
.= (i,j) --> (((product_basis_selector (J,f)) . i),((proj (J,j)) .: ((f ") . j))) by A16, Th54
.= (i,j) --> (V,W) by A16, Th54 ;
dom (Carrier J) = I by PARTFUN1:def 2
.= {i,j} by A1, Th8 ;
then dom (Carrier J) = dom (product_basis_selector (J,f)) by A14, PARTFUN1:def 2;
hence P = product ((i,j) --> (V,W)) by A3, A18, FUNCT_4:19; :: thesis: verum

end;

end;