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 holds
( P in FinMeetCl (product_prebasis J) iff 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 holds
( P in FinMeetCl (product_prebasis J) iff 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 holds
( P in FinMeetCl (product_prebasis J) iff 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 implies ( P in FinMeetCl (product_prebasis J) iff 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 ; :: thesis: ( P in FinMeetCl (product_prebasis J) iff 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)) ) )
hence ( 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)) ) ) by Lm9; :: 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)) ) implies P in FinMeetCl (product_prebasis J) )
given V being Subset of (J . i), W being Subset of (J . j) such that A2: ( V is open & W is open & P = product ((i,j) --> (V,W)) ) ; :: thesis: P in FinMeetCl (product_prebasis J)
ex Y being Subset-Family of (product (Carrier J)) st
( Y c= product_prebasis J & Y is finite & P = Intersect Y )

proof

set V0 = product ((Carrier J) +* (i,V));
set W0 = product ((Carrier J) +* (j,W));
set Y = {(product ((Carrier J) +* (i,V))),(product ((Carrier J) +* (j,W)))};
A3: dom (Carrier J) = I by PARTFUN1:def 2;
( (Carrier J) . i = [#] (J . i) & (Carrier J) . j = [#] (J . j) ) by PENCIL_3:7;
then a4: ( (Carrier J) . i = the carrier of (J . i) & (Carrier J) . j = the carrier of (J . j) ) by STRUCT_0:def 3;
A5: ( product ((Carrier J) +* (i,V)) c= product (Carrier J) & product ((Carrier J) +* (j,W)) c= product (Carrier J) ) by a4, A3, Th39;
then reconsider Y = {(product ((Carrier J) +* (i,V))),(product ((Carrier J) +* (j,W)))} as Subset-Family of (product (Carrier J)) by ZFMISC_1:32;
take Y ; :: thesis: ( Y c= product_prebasis J & Y is finite & P = Intersect Y )
A6: ( product ((Carrier J) +* (i,V)) = product ((i,j) --> (V,((Carrier J) . j))) & product ((Carrier J) +* (j,W)) = product ((i,j) --> (((Carrier J) . i),W)) ) by A1, Th34;
then ( product ((Carrier J) +* (i,V)) = product ((i,j) --> (V,([#] (J . j)))) & product ((Carrier J) +* (j,W)) = product ((i,j) --> (([#] (J . i)),W)) ) by PENCIL_3:7;
then ( product ((Carrier J) +* (i,V)) in product_prebasis J & product ((Carrier J) +* (j,W)) in product_prebasis J ) by A1, A2, A5, Th69;
hence ( Y c= product_prebasis J & Y is finite ) by ZFMISC_1:32; :: thesis: P = Intersect Y
( P c= product ((Carrier J) +* (i,V)) & P c= product ((Carrier J) +* (j,W)) ) by A2, a4, A6, Th28;
then A7: P c= (product ((Carrier J) +* (i,V))) /\ (product ((Carrier J) +* (j,W))) by XBOOLE_1:19;
(product ((Carrier J) +* (i,V))) /\ (product ((Carrier J) +* (j,W))) c= P

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (product ((Carrier J) +* (i,V))) /\ (product ((Carrier J) +* (j,W))) or x in P )
assume x in (product ((Carrier J) +* (i,V))) /\ (product ((Carrier J) +* (j,W))) ; :: thesis: x in P
then A8: ( x in product ((Carrier J) +* (i,V)) & x in product ((Carrier J) +* (j,W)) ) by XBOOLE_0:def 4;
then consider g being Function such that
A9: ( g = x & dom g = dom ((i,j) --> (V,((Carrier J) . j))) ) and
A10: for y being object st y in dom ((i,j) --> (V,((Carrier J) . j))) holds
g . y in ((i,j) --> (V,((Carrier J) . j))) . y by A6, CARD_3:def 5;
A12: dom g = {i,j} by A9, FUNCT_4:62
.= dom ((i,j) --> (V,W)) by FUNCT_4:62 ;
for y being object st y in dom ((i,j) --> (V,W)) holds
g . y in ((i,j) --> (V,W)) . y

proof

let y be object ; :: thesis: ( y in dom ((i,j) --> (V,W)) implies g . y in ((i,j) --> (V,W)) . y )
assume y in dom ((i,j) --> (V,W)) ; :: thesis: g . y in ((i,j) --> (V,W)) . y
then A13: y in {i,j} by FUNCT_4:62;

per cases then ( y = i or y = j ) by TARSKI:def 2;

suppose A14: y = i ; :: thesis: g . y in ((i,j) --> (V,W)) . y

then A15: ((i,j) --> (V,((Carrier J) . j))) . y = V by A1, FUNCT_4:63
.= ((i,j) --> (V,W)) . y by A1, A14, FUNCT_4:63 ;
y in dom ((i,j) --> (V,((Carrier J) . j))) by A13, FUNCT_4:62;
hence g . y in ((i,j) --> (V,W)) . y by A10, A15; :: thesis: verum

end;

suppose A16: y = j ; :: thesis: g . y in ((i,j) --> (V,W)) . y

then A17: ((i,j) --> (((Carrier J) . i),W)) . y = W by FUNCT_4:63
.= ((i,j) --> (V,W)) . y by A16, FUNCT_4:63 ;
y in dom ((i,j) --> (((Carrier J) . i),W)) by A13, FUNCT_4:62;
hence g . y in ((i,j) --> (V,W)) . y by A6, A8, A9, CARD_3:9, A17; :: thesis: verum

end;

end;

end;

hence x in P by A2, A9, A12, CARD_3:9; :: thesis: verum

end;

then P = (product ((Carrier J) +* (i,V))) /\ (product ((Carrier J) +* (j,W))) by A7, XBOOLE_0:def 10;
then P = meet Y by SETFAM_1:11;
hence P = Intersect Y by SETFAM_1:def 9; :: thesis: verum

end;

hence P in FinMeetCl (product_prebasis J) by CANTOR_1:def 3; :: thesis: verum