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;

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;

end;

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)) )

( 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;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

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)) )

( 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;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

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)) )

( 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;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

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)) )

( 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;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