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 )

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

hence
P in FinMeetCl (product_prebasis J)
by CANTOR_1:def 3; :: thesis: verum
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

then P = meet Y by SETFAM_1:11;

hence P = Intersect Y by SETFAM_1:def 9; :: thesis: verum

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

then
P = (product ((Carrier J) +* (i,V))) /\ (product ((Carrier J) +* (j,W)))
by A7, XBOOLE_0:def 10;
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

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

hence
x in P
by A2, A9, A12, CARD_3:9; :: thesis: verum
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;

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

end;

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

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

then P = meet Y by SETFAM_1:11;

hence P = Intersect Y by SETFAM_1:def 9; :: thesis: verum