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 holds
( P in FinMeetCl () 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 ()) st i <> j holds
( P in FinMeetCl () 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 ()) st i <> j holds
( P in FinMeetCl () 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 ()); :: thesis: ( i <> j implies ( P in FinMeetCl () 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 () 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 () 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 () )

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:
ex Y being Subset-Family of (product ()) st
( Y c= product_prebasis J & Y is finite & P = Intersect Y )
proof
set V0 = product (() +* (i,V));
set W0 = product (() +* (j,W));
set Y = {(product (() +* (i,V))),(product (() +* (j,W)))};
A3: dom () = I by PARTFUN1:def 2;
( (Carrier J) . i = [#] (J . i) & () . j = [#] (J . j) ) by PENCIL_3:7;
then a4: ( (Carrier J) . i = the carrier of (J . i) & () . j = the carrier of (J . j) ) by STRUCT_0:def 3;
A5: ( product (() +* (i,V)) c= product () & product (() +* (j,W)) c= product () ) by a4, A3, Th39;
then reconsider Y = {(product (() +* (i,V))),(product (() +* (j,W)))} as Subset-Family of (product ()) by ZFMISC_1:32;
take Y ; :: thesis: ( Y c= product_prebasis J & Y is finite & P = Intersect Y )
A6: ( product (() +* (i,V)) = product ((i,j) --> (V,(() . j))) & product (() +* (j,W)) = product ((i,j) --> ((() . i),W)) ) by ;
then ( product (() +* (i,V)) = product ((i,j) --> (V,([#] (J . j)))) & product (() +* (j,W)) = product ((i,j) --> (([#] (J . i)),W)) ) by PENCIL_3:7;
then ( product (() +* (i,V)) in product_prebasis J & product (() +* (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 c= product (() +* (i,V)) & P c= product (() +* (j,W)) ) by A2, a4, A6, Th28;
then A7: P c= (product (() +* (i,V))) /\ (product (() +* (j,W))) by XBOOLE_1:19;
(product (() +* (i,V))) /\ (product (() +* (j,W))) c= P
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (product (() +* (i,V))) /\ (product (() +* (j,W))) or x in P )
assume x in (product (() +* (i,V))) /\ (product (() +* (j,W))) ; :: thesis: x in P
then A8: ( x in product (() +* (i,V)) & x in product (() +* (j,W)) ) by XBOOLE_0:def 4;
then consider g being Function such that
A9: ( g = x & dom g = dom ((i,j) --> (V,(() . j))) ) and
A10: for y being object st y in dom ((i,j) --> (V,(() . j))) holds
g . y in ((i,j) --> (V,(() . j))) . y by ;
A12: dom g = {i,j} by
.= 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,(() . j))) . y = V by
.= ((i,j) --> (V,W)) . y by ;
y in dom ((i,j) --> (V,(() . j))) by ;
hence g . y in ((i,j) --> (V,W)) . y by ; :: thesis: verum
end;
suppose A16: y = j ; :: thesis: g . y in ((i,j) --> (V,W)) . y
then A17: ((i,j) --> ((() . i),W)) . y = W by FUNCT_4:63
.= ((i,j) --> (V,W)) . y by ;
y in dom ((i,j) --> ((() . i),W)) by ;
hence g . y in ((i,j) --> (V,W)) . y by ; :: thesis: verum
end;
end;
end;
hence x in P by ; :: thesis: verum
end;
then P = (product (() +* (i,V))) /\ (product (() +* (j,W))) by ;
then P = meet Y by SETFAM_1:11;
hence P = Intersect Y by SETFAM_1:def 9; :: thesis: verum
end;
hence P in FinMeetCl () by CANTOR_1:def 3; :: thesis: verum