let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I
for P being Subset of (product ()) st P in FinMeetCl () holds
ex X being Subset-Family of (product ()) ex f being I -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product (() +* ()) )

let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: for P being Subset of (product ()) st P in FinMeetCl () holds
ex X being Subset-Family of (product ()) ex f being I -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product (() +* ()) )

let P be Subset of (product ()); :: thesis: ( P in FinMeetCl () implies ex X being Subset-Family of (product ()) ex f being I -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product (() +* ()) ) )

assume A1: P in FinMeetCl () ; :: thesis: ex X being Subset-Family of (product ()) ex f being I -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product (() +* ()) )

consider Y being Subset-Family of (product ()) such that
A2: ( Y c= product_prebasis J & Y is finite & P = Intersect Y ) by ;
per cases ( ( not Y is empty & meet Y <> {} ) or Y is empty or ( not Y is empty & meet Y = {} ) ) ;
suppose A3: ( not Y is empty & meet Y <> {} ) ; :: thesis: ex X being Subset-Family of (product ()) ex f being I -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product (() +* ()) )

then A4: P = meet Y by ;
defpred S1[ object , object ] means ex i being Element of I ex B being Subset of (J . i) st
( \$2 = i & B is open & \$1 = product (() +* (i,B)) );
A5: for x being object st x in Y holds
ex i being object st
( i in I & S1[x,i] )
proof
let x be object ; :: thesis: ( x in Y implies ex i being object st
( i in I & S1[x,i] ) )

assume x in Y ; :: thesis: ex i being object st
( i in I & S1[x,i] )

then consider i being set , T being TopStruct , V being Subset of T such that
A6: ( i in I & V is open & T = J . i & x = product (() +* (i,V)) ) by ;
take i ; :: thesis: ( i in I & S1[x,i] )
thus i in I by A6; :: thesis: S1[x,i]
reconsider j = i as Element of I by A6;
reconsider V = V as Subset of (J . j) by A6;
take j ; :: thesis: ex B being Subset of (J . j) st
( i = j & B is open & x = product (() +* (j,B)) )

take V ; :: thesis: ( i = j & V is open & x = product (() +* (j,V)) )
thus ( i = j & V is open & x = product (() +* (j,V)) ) by A6; :: thesis: verum
end;
consider g being Function of Y,I such that
A7: for x being object st x in Y holds
S1[x,g . x] from set X = { (meet (g " {i})) where i is Element of I : g " {i} <> {} } ;
{ (meet (g " {i})) where i is Element of I : g " {i} <> {} } c= bool (product ())
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (meet (g " {i})) where i is Element of I : g " {i} <> {} } or x in bool (product ()) )
assume x in { (meet (g " {i})) where i is Element of I : g " {i} <> {} } ; :: thesis: x in bool (product ())
then consider i being Element of I such that
A8: ( x = meet (g " {i}) & g " {i} <> {} ) ;
reconsider Z = g " {i} as Subset-Family of (product ()) by XBOOLE_1:1;
meet Z is Subset of (product ()) ;
hence x in bool (product ()) by A8; :: thesis: verum
end;
then reconsider X = { (meet (g " {i})) where i is Element of I : g " {i} <> {} } as Subset-Family of (product ()) ;
take X ; :: thesis: ex f being I -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product (() +* ()) )

defpred S2[ object , object ] means ex i being Element of I st
( \$2 = i & \$1 = meet (g " {i}) & g " {i} <> {} );
A9: for x being object st x in X holds
ex i being object st
( i in I & S2[x,i] )
proof
let x be object ; :: thesis: ( x in X implies ex i being object st
( i in I & S2[x,i] ) )

assume x in X ; :: thesis: ex i being object st
( i in I & S2[x,i] )

then consider i being Element of I such that
A10: ( x = meet (g " {i}) & g " {i} <> {} ) ;
take i ; :: thesis: ( i in I & S2[x,i] )
thus i in I ; :: thesis: S2[x,i]
take i ; :: thesis: ( i = i & x = meet (g " {i}) & g " {i} <> {} )
thus ( i = i & x = meet (g " {i}) & g " {i} <> {} ) by A10; :: thesis: verum
end;
consider f being Function of X,I such that
A11: for x being object st x in X holds
S2[x,f . x] from A12: ( dom f = X & rng f c= I ) by FUNCT_2:def 1;
for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
proof
let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume A13: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then consider i1 being Element of I such that
A14: ( f . x1 = i1 & x1 = meet (g " {i1}) & g " {i1} <> {} ) by A11;
ex i2 being Element of I st
( f . x2 = i2 & x2 = meet (g " {i2}) & g " {i2} <> {} ) by ;
hence x1 = x2 by ; :: thesis: verum
end;
then reconsider f = f as I -valued one-to-one Function by FUNCT_1:def 4;
take f ; :: thesis: ( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product (() +* ()) )
A16: for i being Element of I
for S being non empty set st g " {i} <> {} & S in g " {i} holds
ex V being non empty open Subset of (J . i) st S = product (() +* (i,V))
proof
let i be Element of I; :: thesis: for S being non empty set st g " {i} <> {} & S in g " {i} holds
ex V being non empty open Subset of (J . i) st S = product (() +* (i,V))

let S be non empty set ; :: thesis: ( g " {i} <> {} & S in g " {i} implies ex V being non empty open Subset of (J . i) st S = product (() +* (i,V)) )
assume a17: ( g " {i} <> {} & S in g " {i} ) ; :: thesis: ex V being non empty open Subset of (J . i) st S = product (() +* (i,V))
then A17: ( S in Y & g . S in {i} ) by FUNCT_2:38;
then consider j being set , T being TopStruct , V being Subset of T such that
A18: ( j in I & V is open & T = J . j ) and
A19: S = product (() +* (j,V)) by ;
a20: dom () = I by PARTFUN1:def 2;
per cases ( V <> () . j or V = () . j ) ;
suppose A21: V <> () . j ; :: thesis: ex V being non empty open Subset of (J . i) st S = product (() +* (i,V))
A22: not V is empty by ;
A23: i = j
proof
g . S = i by ;
then consider k being Element of I, B being Subset of (J . k) such that
A24: ( i = k & B is open ) and
A25: S = product (() +* (k,B)) by ;
not B is empty by ;
hence i = j by A19, A18, a20, A21, A22, A24, A25, Th42; :: thesis: verum
end;
then reconsider V = V as non empty open Subset of (J . i) by ;
take V ; :: thesis: S = product (() +* (i,V))
thus S = product (() +* (i,V)) by ; :: thesis: verum
end;
suppose V = () . j ; :: thesis: ex V being non empty open Subset of (J . i) st S = product (() +* (i,V))
then A26: S = product () by
.= product (() +* (i,(() . i))) by FUNCT_7:35 ;
take [#] (J . i) ; :: thesis: S = product (() +* (i,([#] (J . i))))
thus S = product (() +* (i,([#] (J . i)))) by ; :: thesis: verum
end;
end;
end;
A27: not X is empty
proof
A28: ex i being Element of I st g " {i} <> {}
proof
set A = the Element of Y;
consider i being Element of I, B being Subset of (J . i) such that
A29: ( g . the Element of Y = i & B is open & the Element of Y = product (() +* (i,B)) ) by A3, A7;
take i ; :: thesis: g " {i} <> {}
g . the Element of Y in {i} by ;
hence g " {i} <> {} by ; :: thesis: verum
end;
ex x being object st x in X
proof
consider i being Element of I such that
A30: g " {i} <> {} by A28;
meet (g " {i}) in X by A30;
hence ex x being object st x in X ; :: thesis: verum
end;
hence not X is empty ; :: thesis: verum
end;
A31: for x being Element of X st x = meet (g " {(f . x)}) & g " {(f . x)} <> {} & x <> {} holds
ex Z being Subset-Family of (J . (In ((f . x),I))) st
( Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product ()) : V in g " {(f . x)} } & Z is open & Z is finite & not Z is empty & x = product (() +* ((f . x),(meet Z))) )
proof
let x be Element of X; :: thesis: ( x = meet (g " {(f . x)}) & g " {(f . x)} <> {} & x <> {} implies ex Z being Subset-Family of (J . (In ((f . x),I))) st
( Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product ()) : V in g " {(f . x)} } & Z is open & Z is finite & not Z is empty & x = product (() +* ((f . x),(meet Z))) ) )

set i = In ((f . x),I);
a32: f . x in rng f by ;
then A32: In ((f . x),I) = f . x by SUBSET_1:def 8;
assume A33: ( x = meet (g " {(f . x)}) & g " {(f . x)} <> {} & x <> {} ) ; :: thesis: ex Z being Subset-Family of (J . (In ((f . x),I))) st
( Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product ()) : V in g " {(f . x)} } & Z is open & Z is finite & not Z is empty & x = product (() +* ((f . x),(meet Z))) )

set Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product ()) : V in g " {(f . x)} } ;
{ ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product ()) : V in g " {(f . x)} } c= bool the carrier of (J . (In ((f . x),I)))
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product ()) : V in g " {(f . x)} } or y in bool the carrier of (J . (In ((f . x),I))) )
assume y in { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product ()) : V in g " {(f . x)} } ; :: thesis: y in bool the carrier of (J . (In ((f . x),I)))
then ex V being Subset of (product ()) st
( y = (proj (J,(In ((f . x),I)))) .: V & V in g " {(f . x)} ) ;
hence y in bool the carrier of (J . (In ((f . x),I))) ; :: thesis: verum
end;
then reconsider Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product ()) : V in g " {(f . x)} } as Subset-Family of (J . (In ((f . x),I))) ;
take Z ; :: thesis: ( Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product ()) : V in g " {(f . x)} } & Z is open & Z is finite & not Z is empty & x = product (() +* ((f . x),(meet Z))) )
thus Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product ()) : V in g " {(f . x)} } ; :: thesis: ( Z is open & Z is finite & not Z is empty & x = product (() +* ((f . x),(meet Z))) )
for A being Subset of (J . (In ((f . x),I))) st A in Z holds
A is open
proof
let A be Subset of (J . (In ((f . x),I))); :: thesis: ( A in Z implies A is open )
assume A in Z ; :: thesis: A is open
then consider V being Subset of (product ()) such that
A35: ( A = (proj (J,(In ((f . x),I)))) .: V & V in g " {(f . x)} ) ;
( V in Y & ( V is empty or not V is empty ) ) by A35;
hence A is open by ; :: thesis: verum
end;
hence Z is open by TOPS_2:def 1; :: thesis: ( Z is finite & not Z is empty & x = product (() +* ((f . x),(meet Z))) )
defpred S3[ object , object ] means ex V being Subset of (product ()) st
( \$1 = V & \$2 = (proj (J,(In ((f . x),I)))) .: V );
A37: for y, z1, z2 being object st y in g " {(In ((f . x),I))} & S3[y,z1] & S3[y,z2] holds
z1 = z2 ;
A38: for y being object st y in g " {(In ((f . x),I))} holds
ex z being object st S3[y,z]
proof
let y be object ; :: thesis: ( y in g " {(In ((f . x),I))} implies ex z being object st S3[y,z] )
assume y in g " {(In ((f . x),I))} ; :: thesis: ex z being object st S3[y,z]
then y in Y ;
then reconsider V = y as Subset of (product ()) ;
take (proj (J,(In ((f . x),I)))) .: V ; :: thesis: S3[y,(proj (J,(In ((f . x),I)))) .: V]
take V ; :: thesis: ( y = V & (proj (J,(In ((f . x),I)))) .: V = (proj (J,(In ((f . x),I)))) .: V )
thus ( y = V & (proj (J,(In ((f . x),I)))) .: V = (proj (J,(In ((f . x),I)))) .: V ) ; :: thesis: verum
end;
consider h being Function such that
A39: ( dom h = g " {(In ((f . x),I))} & ( for y being object st y in g " {(In ((f . x),I))} holds
S3[y,h . y] ) ) from a45: for y being object holds
( y in rng h iff y in Z )
proof
let y be object ; :: thesis: ( y in rng h iff y in Z )
hereby :: thesis: ( y in Z implies y in rng h )
assume y in rng h ; :: thesis: y in Z
then consider z being object such that
A40: ( z in dom h & y = h . z ) by FUNCT_1:def 3;
ex V being Subset of (product ()) st
( z = V & h . z = (proj (J,(In ((f . x),I)))) .: V ) by ;
hence y in Z by ; :: thesis: verum
end;
assume y in Z ; :: thesis: y in rng h
then consider V being Subset of (product ()) such that
A42: ( y = (proj (J,(In ((f . x),I)))) .: V & V in g " {(f . x)} ) ;
A43: V in dom h by ;
ex V0 being Subset of (product ()) st
( V = V0 & h . V = (proj (J,(In ((f . x),I)))) .: V0 ) by ;
hence y in rng h by ; :: thesis: verum
end;
then rng h = Z by TARSKI:2;
hence Z is finite by ; :: thesis: ( not Z is empty & x = product (() +* ((f . x),(meet Z))) )
h . the Element of g " {(f . x)} in rng h by ;
hence A46: not Z is empty by a45; :: thesis: x = product (() +* ((f . x),(meet Z)))
a47: dom () = I by PARTFUN1:def 2;
then A47: In ((f . x),I) in dom () ;
for y being object holds
( y in meet (g " {(In ((f . x),I))}) iff y in product (() +* ((In ((f . x),I)),(meet Z))) )
proof
let y be object ; :: thesis: ( y in meet (g " {(In ((f . x),I))}) iff y in product (() +* ((In ((f . x),I)),(meet Z))) )
hereby :: thesis: ( y in product (() +* ((In ((f . x),I)),(meet Z))) implies y in meet (g " {(In ((f . x),I))}) )
assume A49: y in meet (g " {(In ((f . x),I))}) ; :: thesis: y in product (() +* ((In ((f . x),I)),(meet Z)))
set S0 = the Element of g " {(In ((f . x),I))};
not the Element of g " {(In ((f . x),I))} is empty by ;
then consider V0 being non empty open Subset of (J . (In ((f . x),I))) such that
A50: the Element of g " {(In ((f . x),I))} = product (() +* ((In ((f . x),I)),V0)) by ;
y in product (() +* ((In ((f . x),I)),V0)) by ;
then consider f0 being Function such that
A51: ( y = f0 & dom f0 = dom (() +* ((In ((f . x),I)),V0)) ) and
A52: for z being object st z in dom (() +* ((In ((f . x),I)),V0)) holds
f0 . z in (() +* ((In ((f . x),I)),V0)) . z by CARD_3:def 5;
now :: thesis: ex f0 being Function st
( y = f0 & dom f0 = dom (() +* ((In ((f . x),I)),(meet Z))) & ( for z being object st z in dom (() +* ((In ((f . x),I)),(meet Z))) holds
f0 . z in (() +* ((In ((f . x),I)),(meet Z))) . z ) )
take f0 = f0; :: thesis: ( y = f0 & dom f0 = dom (() +* ((In ((f . x),I)),(meet Z))) & ( for z being object st z in dom (() +* ((In ((f . x),I)),(meet Z))) holds
b2 . b3 in (() +* ((In ((f . x),I)),(meet Z))) . b3 ) )

thus y = f0 by A51; :: thesis: ( dom f0 = dom (() +* ((In ((f . x),I)),(meet Z))) & ( for z being object st z in dom (() +* ((In ((f . x),I)),(meet Z))) holds
b2 . b3 in (() +* ((In ((f . x),I)),(meet Z))) . b3 ) )

thus dom f0 = dom () by
.= dom (() +* ((In ((f . x),I)),(meet Z))) by FUNCT_7:30 ; :: thesis: for z being object st z in dom (() +* ((In ((f . x),I)),(meet Z))) holds
b2 . b3 in (() +* ((In ((f . x),I)),(meet Z))) . b3

let z be object ; :: thesis: ( z in dom (() +* ((In ((f . x),I)),(meet Z))) implies b1 . b2 in (() +* ((In ((f . x),I)),(meet Z))) . b2 )
assume z in dom (() +* ((In ((f . x),I)),(meet Z))) ; :: thesis: b1 . b2 in (() +* ((In ((f . x),I)),(meet Z))) . b2
then A53: z in dom () by FUNCT_7:30;
per cases ( z <> In ((f . x),I) or z = In ((f . x),I) ) ;
suppose A54: z <> In ((f . x),I) ; :: thesis: b1 . b2 in (() +* ((In ((f . x),I)),(meet Z))) . b2
then A55: (() +* ((In ((f . x),I)),(meet Z))) . z = () . z by FUNCT_7:32
.= (() +* ((In ((f . x),I)),V0)) . z by ;
z in dom (() +* ((In ((f . x),I)),V0)) by ;
hence f0 . z in (() +* ((In ((f . x),I)),(meet Z))) . z by ; :: thesis: verum
end;
suppose A56: z = In ((f . x),I) ; :: thesis: b1 . b2 in (() +* ((In ((f . x),I)),(meet Z))) . b2
then A57: ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . z = meet Z by ;
for S being set st S in Z holds
f0 . z in S
proof
let S be set ; :: thesis: ( S in Z implies f0 . z in S )
assume S in Z ; :: thesis: f0 . z in S
then consider S1 being Subset of (product ()) such that
A58: ( S = (proj (J,(In ((f . x),I)))) .: S1 & S1 in g " {(f . x)} ) ;
not S1 is empty by ;
then consider V1 being non empty open Subset of (J . (In ((f . x),I))) such that
A59: S1 = product (() +* ((In ((f . x),I)),V1)) by ;
V1 c= the carrier of (J . (In ((f . x),I))) ;
then V1 c= [#] (J . (In ((f . x),I))) by STRUCT_0:def 3;
then A60: V1 c= () . (In ((f . x),I)) by PENCIL_3:7;
proj (J,(In ((f . x),I))) = proj ((),(In ((f . x),I))) by WAYBEL18:def 4;
then A61: S = V1 by A58, A59, A60, a47, Th43;
y in S1 by ;
then consider f1 being Function such that
A62: ( y = f1 & dom f1 = dom (() +* ((In ((f . x),I)),V1)) ) and
A63: for a being object st a in dom (() +* ((In ((f . x),I)),V1)) holds
f1 . a in (() +* ((In ((f . x),I)),V1)) . a by ;
In ((f . x),I) in dom (() +* ((In ((f . x),I)),V1)) by ;
then f1 . (In ((f . x),I)) in (() +* ((In ((f . x),I)),V1)) . (In ((f . x),I)) by A63;
hence f0 . z in S by ; :: thesis: verum
end;
hence f0 . z in (() +* ((In ((f . x),I)),(meet Z))) . z by ; :: thesis: verum
end;
end;
end;
hence y in product (() +* ((In ((f . x),I)),(meet Z))) by CARD_3:def 5; :: thesis: verum
end;
assume A64: y in product (() +* ((In ((f . x),I)),(meet Z))) ; :: thesis: y in meet (g " {(In ((f . x),I))})
for S being set st S in g " {(In ((f . x),I))} holds
y in S
proof
let S be set ; :: thesis: ( S in g " {(In ((f . x),I))} implies y in S )
assume A65: S in g " {(In ((f . x),I))} ; :: thesis: y in S
not S is empty by ;
then consider V being non empty open Subset of (J . (In ((f . x),I))) such that
A66: S = product (() +* ((In ((f . x),I)),V)) by ;
V c= the carrier of (J . (In ((f . x),I))) ;
then V c= [#] (J . (In ((f . x),I))) by STRUCT_0:def 3;
then A67: V c= () . (In ((f . x),I)) by PENCIL_3:7;
proj (J,(In ((f . x),I))) = proj ((),(In ((f . x),I))) by WAYBEL18:def 4;
then A68: (proj (J,(In ((f . x),I)))) .: S = V by ;
S in Y by A65;
then V in Z by ;
then product (() +* ((In ((f . x),I)),(meet Z))) c= product (() +* ((In ((f . x),I)),V)) by ;
hence y in S by ; :: thesis: verum
end;
hence y in meet (g " {(In ((f . x),I))}) by ; :: thesis: verum
end;
hence x = product (() +* ((f . x),(meet Z))) by ; :: thesis: verum
end;
for x being object st x in X holds
x in product_prebasis J
proof
let x be object ; :: thesis: ( x in X implies x in product_prebasis J )
assume A69: x in X ; :: thesis:
per cases ( x <> {} or x = {} ) ;
suppose A70: x <> {} ; :: thesis:
ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product (() +* (i,V)) )
proof
consider i being Element of I such that
A71: ( f . x = i & x = meet (g " {i}) & g " {i} <> {} ) by ;
consider Z being Subset-Family of (J . (In ((f . x),I))) such that
Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product ()) : V in g " {(f . x)} } and
A72: ( Z is open & Z is finite & not Z is empty ) and
A73: x = product (() +* ((f . x),(meet Z))) by A31, A69, A70, A71;
set W = meet Z;
take i ; :: thesis: ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product (() +* (i,V)) )

take J . (In ((f . x),I)) ; :: thesis: ex V being Subset of (J . (In ((f . x),I))) st
( i in I & V is open & J . (In ((f . x),I)) = J . i & x = product (() +* (i,V)) )

take meet Z ; :: thesis: ( i in I & meet Z is open & J . (In ((f . x),I)) = J . i & x = product (() +* (i,(meet Z))) )
thus ( i in I & meet Z is open & J . (In ((f . x),I)) = J . i & x = product (() +* (i,(meet Z))) ) by ; :: thesis: verum
end;
hence x in product_prebasis J by ; :: thesis: verum
end;
end;
end;
hence X c= product_prebasis J by TARSKI:def 3; :: thesis: ( X is finite & P = Intersect X & dom f = X & P = product (() +* ()) )
for x being object holds
( x in meet X iff x in meet Y )
proof
let x be object ; :: thesis: ( x in meet X iff x in meet Y )
hereby :: thesis: ( x in meet Y implies x in meet X )
assume A74: x in meet X ; :: thesis: x in meet Y
for Sy being set st Sy in Y holds
x in Sy
proof
let Sy be set ; :: thesis: ( Sy in Y implies x in Sy )
assume A75: Sy in Y ; :: thesis: x in Sy
then consider i being Element of I, B being Subset of (J . i) such that
A76: ( g . Sy = i & B is open & Sy = product (() +* (i,B)) ) by A7;
g . Sy in {i} by ;
then A77: Sy in g " {i} by ;
then meet (g " {i}) in X ;
then A78: x in meet (g " {i}) by ;
meet (g " {i}) c= Sy by ;
hence x in Sy by A78; :: thesis: verum
end;
hence x in meet Y by ; :: thesis: verum
end;
assume A79: x in meet Y ; :: thesis: x in meet X
for Sx being set st Sx in X holds
x in Sx
proof
let Sx be set ; :: thesis: ( Sx in X implies x in Sx )
assume Sx in X ; :: thesis: x in Sx
then consider i being Element of I such that
A80: ( Sx = meet (g " {i}) & g " {i} <> {} ) ;
for A being set st A in g " {i} holds
x in A by ;
hence x in Sx by ; :: thesis: verum
end;
hence x in meet X by ; :: thesis: verum
end;
then A81: meet X = meet Y by TARSKI:2;
thus X is finite :: thesis: ( P = Intersect X & dom f = X & P = product (() +* ()) )
proof
set S = { (g " {i}) where i is Element of I : i in rng g } ;
a82: { (g " {i}) where i is Element of I : i in rng g } is a_partition of Y by Th5;
defpred S3[ object , object ] means ex M being set st
( \$1 = M & \$2 = meet M );
A83: for A being object st A in { (g " {i}) where i is Element of I : i in rng g } holds
ex B being object st
( B in X & S3[A,B] )
proof
let A be object ; :: thesis: ( A in { (g " {i}) where i is Element of I : i in rng g } implies ex B being object st
( B in X & S3[A,B] ) )

assume A in { (g " {i}) where i is Element of I : i in rng g } ; :: thesis: ex B being object st
( B in X & S3[A,B] )

then consider i being Element of I such that
A84: ( A = g " {i} & i in rng g ) ;
take meet (g " {i}) ; :: thesis: ( meet (g " {i}) in X & S3[A, meet (g " {i})] )
consider x being object such that
A85: ( x in Y & g . x = i ) by ;
i in {i} by TARSKI:def 1;
then x in g " {i} by ;
hence meet (g " {i}) in X ; :: thesis: S3[A, meet (g " {i})]
take g " {i} ; :: thesis: ( A = g " {i} & meet (g " {i}) = meet (g " {i}) )
thus ( A = g " {i} & meet (g " {i}) = meet (g " {i}) ) by A84; :: thesis: verum
end;
consider h being Function of { (g " {i}) where i is Element of I : i in rng g } ,X such that
A86: for A being object st A in { (g " {i}) where i is Element of I : i in rng g } holds
S3[A,h . A] from for B being object st B in X holds
ex A being object st
( A in { (g " {i}) where i is Element of I : i in rng g } & B = h . A )
proof
let B be object ; :: thesis: ( B in X implies ex A being object st
( A in { (g " {i}) where i is Element of I : i in rng g } & B = h . A ) )

assume B in X ; :: thesis: ex A being object st
( A in { (g " {i}) where i is Element of I : i in rng g } & B = h . A )

then consider i being Element of I such that
A87: ( B = meet (g " {i}) & g " {i} <> {} ) ;
take g " {i} ; :: thesis: ( g " {i} in { (g " {i}) where i is Element of I : i in rng g } & B = h . (g " {i}) )
consider x being object such that
A88: x in g " {i} by ;
( x in Y & g . x in {i} ) by ;
then A90: g . x = i by TARSKI:def 1;
dom g = Y by FUNCT_2:def 1;
then i in rng g by ;
hence g " {i} in { (g " {i}) where i is Element of I : i in rng g } ; :: thesis: B = h . (g " {i})
then ex M being set st
( g " {i} = M & h . (g " {i}) = meet M ) by A86;
hence B = h . (g " {i}) by A87; :: thesis: verum
end;
then rng h = X by FUNCT_2:10;
hence X is finite by ; :: thesis: verum
end;
thus P = Intersect X by ; :: thesis: ( dom f = X & P = product (() +* ()) )
thus dom f = X by FUNCT_2:def 1; :: thesis: P = product (() +* ())
set F = () +* ();
for x being object holds
( x in meet X iff x in product (() +* ()) )
proof
let x be object ; :: thesis: ( x in meet X iff x in product (() +* ()) )
A92: I = I \/ (rng f) by XBOOLE_1:12
.= (dom ()) \/ (rng f) by PARTFUN1:def 2
.= (dom ()) \/ (dom ()) by PARTFUN1:def 2
.= dom (() +* ()) by FUNCT_4:def 1 ;
hereby :: thesis: ( x in product (() +* ()) implies x in meet X )
assume A93: x in meet X ; :: thesis: x in product (() +* ())
consider A0 being object such that
A94: A0 in X by ;
reconsider A0 = A0 as set by TARSKI:1;
consider i0 being Element of I such that
A95: ( f . A0 = i0 & A0 = meet (g " {i0}) & g " {i0} <> {} ) by ;
A0 <> {} by ;
then consider Z0 being Subset-Family of (J . (In ((f . A0),I))) such that
Z0 = { ((proj (J,(In ((f . A0),I)))) .: V) where V is Subset of (product ()) : V in g " {(f . A0)} } and
( Z0 is open & Z0 is finite & not Z0 is empty ) and
A96: A0 = product (() +* ((f . A0),(meet Z0))) by ;
x in A0 by ;
then consider h being Function such that
A97: ( x = h & dom h = dom (() +* ((f . A0),(meet Z0))) ) and
A98: for y being object st y in dom (() +* ((f . A0),(meet Z0))) holds
h . y in (() +* ((f . A0),(meet Z0))) . y by ;
A99: dom h = I by ;
A100: dom h = dom (() +* ()) by ;
for y being object st y in dom (() +* ()) holds
h . y in (() +* ()) . y
proof
let y be object ; :: thesis: ( y in dom (() +* ()) implies h . y in (() +* ()) . y )
assume y in dom (() +* ()) ; :: thesis: h . y in (() +* ()) . y
then reconsider i = y as Element of I by A92;
i in dom h by A99;
then A101: i in dom () by ;
per cases ( y in rng f or not y in rng f ) ;
suppose A102: y in rng f ; :: thesis: h . y in (() +* ()) . y
then y in dom () by PARTFUN1:def 2;
then ((Carrier J) +* ()) . y = () . i by FUNCT_4:13;
then A103: ((Carrier J) +* ()) . y = (proj (J,i)) .: ((f ") . i) by ;
consider A being object such that
A104: ( A in X & f . A = i ) by ;
reconsider A = A as set by TARSKI:1;
consider j being Element of I such that
A105: ( f . A = j & A = meet (g " {j}) & g " {j} <> {} ) by ;
A <> {} by ;
then consider Z being Subset-Family of (J . (In ((f . A),I))) such that
Z = { ((proj (J,(In ((f . A),I)))) .: V) where V is Subset of (product ()) : V in g " {(f . A)} } and
( Z is open & Z is finite & not Z is empty ) and
A106: A = product (() +* ((f . A),(meet Z))) by ;
reconsider Z = Z as Subset-Family of (J . i) by A104;
a107: h in A by ;
dom (() +* ((f . A),(meet Z))) = I by PARTFUN1:def 2;
then h . i in (() +* ((f . A),(meet Z))) . i by ;
then A108: h . i in meet Z by ;
ex z being object st
( z in dom (proj (J,i)) & z in meet (g " {i}) & (proj (J,i)) . z = h . i )
proof
set z0 = the Element of product ();
set z = the Element of product () +* (i,(h . i));
take the Element of product () +* (i,(h . i)) ; :: thesis: ( the Element of product () +* (i,(h . i)) in dom (proj (J,i)) & the Element of product () +* (i,(h . i)) in meet (g " {i}) & (proj (J,i)) . ( the Element of product () +* (i,(h . i))) = h . i )
meet Z c= the carrier of (J . i) ;
then meet Z c= [#] (J . i) by STRUCT_0:def 3;
then A109: meet Z c= () . i by PENCIL_3:7;
A110: the Element of product () +* (i,(h . i)) in product (() +* (i,(meet Z))) by ;
product (() +* (i,(meet Z))) c= product () by ;
then the Element of product () +* (i,(h . i)) in product () by A110;
then A111: the Element of product () +* (i,(h . i)) in dom (proj ((),i)) by CARD_3:def 16;
hence ( the Element of product () +* (i,(h . i)) in dom (proj (J,i)) & the Element of product () +* (i,(h . i)) in meet (g " {i}) ) by ; :: thesis: (proj (J,i)) . ( the Element of product () +* (i,(h . i))) = h . i
A112: i in dom the Element of product () by ;
thus (proj (J,i)) . ( the Element of product () +* (i,(h . i))) = (proj ((),i)) . ( the Element of product () +* (i,(h . i))) by WAYBEL18:def 4
.= ( the Element of product () +* (i,(h . i))) . i by
.= h . i by ; :: thesis: verum
end;
then h . i in (proj (J,i)) .: (meet (g " {i})) by FUNCT_1:def 6;
hence h . y in (() +* ()) . y by ; :: thesis: verum
end;
suppose not y in rng f ; :: thesis: h . y in (() +* ()) . y
then not y in dom () ;
then A114: ((Carrier J) +* ()) . y = () . y by FUNCT_4:11;
reconsider Z0 = Z0 as Subset-Family of (J . i0) by A95;
meet Z0 c= the carrier of (J . i0) ;
then meet Z0 c= [#] (J . i0) by STRUCT_0:def 3;
then A115: meet Z0 c= () . i0 by PENCIL_3:7;
i0 in I ;
then i0 in dom () by PARTFUN1:def 2;
then A116: product (() +* (i0,(meet Z0))) c= product () by ;
h in product (() +* (i0,(meet Z0))) by ;
hence h . y in (() +* ()) . y by ; :: thesis: verum
end;
end;
end;
hence x in product (() +* ()) by ; :: thesis: verum
end;
assume x in product (() +* ()) ; :: thesis: x in meet X
then consider h being Function such that
A117: ( h = x & dom h = dom (() +* ()) ) and
A118: for y being object st y in dom (() +* ()) holds
h . y in (() +* ()) . y by CARD_3:def 5;
for A being set st A in X holds
h in A
proof
let A be set ; :: thesis: ( A in X implies h in A )
assume A119: A in X ; :: thesis: h in A
then consider i being Element of I such that
A120: ( f . A = i & A = meet (g " {i}) & g " {i} <> {} ) by A11;
A121: (f ") . i = A by ;
A <> {} by ;
then consider Z being Subset-Family of (J . (In ((f . A),I))) such that
A122: Z = { ((proj (J,(In ((f . A),I)))) .: V) where V is Subset of (product ()) : V in g " {(f . A)} } and
( Z is open & Z is finite & not Z is empty ) and
A124: A = product (() +* ((f . A),(meet Z))) by ;
A125: dom h = dom (() +* ((f . A),(meet Z))) by ;
for y being object st y in dom (() +* ((f . A),(meet Z))) holds
h . y in (() +* ((f . A),(meet Z))) . y
proof
let y be object ; :: thesis: ( y in dom (() +* ((f . A),(meet Z))) implies h . y in (() +* ((f . A),(meet Z))) . y )
assume A126: y in dom (() +* ((f . A),(meet Z))) ; :: thesis: h . y in (() +* ((f . A),(meet Z))) . y
per cases ( y <> i or y = i ) ;
suppose y <> i ; :: thesis: h . y in (() +* ((f . A),(meet Z))) . y
then A127: ((Carrier J) +* ((f . A),(meet Z))) . y = () . y by ;
A128: y in dom () by ;
A129: h . y in (() +* ()) . y by ;
per cases ( y in rng f or not y in rng f ) ;
suppose A130: y in rng f ; :: thesis: h . y in (() +* ((f . A),(meet Z))) . y
then reconsider i0 = y as Element of I ;
y in dom () by ;
then (() +* ()) . y = () . i0 by FUNCT_4:13
.= (proj (J,i0)) .: ((f ") . i0) by ;
then ((Carrier J) +* ()) . y c= rng (proj (J,i0)) by RELAT_1:111;
then ((Carrier J) +* ()) . y c= rng (proj ((),i0)) by WAYBEL18:def 4;
then ((Carrier J) +* ()) . y c= () . i0 by ;
hence h . y in (() +* ((f . A),(meet Z))) . y by ; :: thesis: verum
end;
suppose not y in rng f ; :: thesis: h . y in (() +* ((f . A),(meet Z))) . y
then not y in dom () ;
hence h . y in (() +* ((f . A),(meet Z))) . y by ; :: thesis: verum
end;
end;
end;
suppose A131: y = i ; :: thesis: h . y in (() +* ((f . A),(meet Z))) . y
i in I ;
then a132: i in dom () by PARTFUN1:def 2;
A133: i in rng f by ;
then i in dom () by PARTFUN1:def 2;
then A134: (() +* ()) . i = () . i by FUNCT_4:13
.= (proj (J,i)) .: (meet (g " {i})) by ;
reconsider G = g " {i} as Subset-Family of (product ()) by XBOOLE_1:1;
h . i in (proj (J,i)) .: (meet (g " {i})) by ;
then h . i in meet { ((proj (J,i)) .: B) where B is Subset of (product ()) : B in G } by ;
hence h . y in (() +* ((f . A),(meet Z))) . y by ; :: thesis: verum
end;
end;
end;
hence h in A by ; :: thesis: verum
end;
hence x in meet X by ; :: thesis: verum
end;
hence P = product (() +* ()) by ; :: thesis: verum
end;
suppose A136: Y is empty ; :: thesis: ex X being Subset-Family of (product ()) ex f being I -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product (() +* ()) )

reconsider f = the empty Function as I -valued one-to-one Function by ;
take Y ; :: thesis: ex f being I -valued one-to-one Function st
( Y c= product_prebasis J & Y is finite & P = Intersect Y & dom f = Y & P = product (() +* ()) )

take f ; :: thesis: ( Y c= product_prebasis J & Y is finite & P = Intersect Y & dom f = Y & P = product (() +* ()) )
thus ( Y c= product_prebasis J & Y is finite & P = Intersect Y ) by A2; :: thesis: ( dom f = Y & P = product (() +* ()) )
thus dom f = Y by A136; :: thesis: P = product (() +* ())
product_basis_selector (J,f) is empty ;
hence P = product (() +* ()) by ; :: thesis: verum
end;
suppose ( not Y is empty & meet Y = {} ) ; :: thesis: ex X being Subset-Family of (product ()) ex f being I -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product (() +* ()) )

then A138: P = {} by ;
set i = the Element of I;
set V = the empty Subset of (J . the Element of I);
a139: dom () = I by PARTFUN1:def 2;
then A140: product (() +* ( the Element of I, the empty Subset of (J . the Element of I))) = {} by Th36;
then product (() +* ( the Element of I, the empty Subset of (J . the Element of I))) in product_prebasis J by Th56;
then reconsider A = product (() +* ( the Element of I, the empty Subset of (J . the Element of I))) as Subset of (product ()) ;
set X = {A};
set f = A .--> the Element of I;
take {A} ; :: thesis: ex f being I -valued one-to-one Function st
( {A} c= product_prebasis J & {A} is finite & P = Intersect {A} & dom f = {A} & P = product (() +* ()) )

take A .--> the Element of I ; :: thesis: ( {A} c= product_prebasis J & {A} is finite & P = Intersect {A} & dom (A .--> the Element of I) = {A} & P = product (() +* (product_basis_selector (J,(A .--> the Element of I)))) )
thus ( {A} c= product_prebasis J & {A} is finite ) by ; :: thesis: ( P = Intersect {A} & dom (A .--> the Element of I) = {A} & P = product (() +* (product_basis_selector (J,(A .--> the Element of I)))) )
{} in {A} by ;
then meet {A} = {} by SETFAM_1:4;
hence P = Intersect {A} by ; :: thesis: ( dom (A .--> the Element of I) = {A} & P = product (() +* (product_basis_selector (J,(A .--> the Element of I)))) )
thus dom (A .--> the Element of I) = dom ({A} --> the Element of I) by FUNCOP_1:def 9
.= {A} ; :: thesis: P = product (() +* (product_basis_selector (J,(A .--> the Element of I))))
set F = () +* (product_basis_selector (J,(A .--> the Element of I)));
ex j being object st
( j in dom (() +* (product_basis_selector (J,(A .--> the Element of I)))) & (() +* (product_basis_selector (J,(A .--> the Element of I)))) . j = {} )
proof
take the Element of I ; :: thesis: ( the Element of I in dom (() +* (product_basis_selector (J,(A .--> the Element of I)))) & (() +* (product_basis_selector (J,(A .--> the Element of I)))) . the Element of I = {} )
the Element of I in (dom ()) \/ (dom (product_basis_selector (J,(A .--> the Element of I)))) by ;
hence the Element of I in dom (() +* (product_basis_selector (J,(A .--> the Element of I)))) by FUNCT_4:def 1; :: thesis: (() +* (product_basis_selector (J,(A .--> the Element of I)))) . the Element of I = {}
the Element of I in { the Element of I} by TARSKI:def 1;
then the Element of I in rng ({A} --> the Element of I) by FUNCOP_1:8;
then A142: the Element of I in rng (A .--> the Element of I) by FUNCOP_1:def 9;
then the Element of I in dom (product_basis_selector (J,(A .--> the Element of I))) by PARTFUN1:def 2;
hence (() +* (product_basis_selector (J,(A .--> the Element of I)))) . the Element of I = (product_basis_selector (J,(A .--> the Element of I))) . the Element of I by FUNCT_4:13
.= (proj (J, the Element of I)) .: (((A .--> the Element of I) ") . the Element of I) by
.= (proj (J, the Element of I)) .: (( the Element of I .--> A) . the Element of I) by NECKLACE:9
.= (proj (J, the Element of I)) .: A by FUNCOP_1:72
.= {} by A140 ;
:: thesis: verum
end;
then {} in rng (() +* (product_basis_selector (J,(A .--> the Element of I)))) by FUNCT_1:def 3;
hence P = product (() +* (product_basis_selector (J,(A .--> the Element of I)))) by ; :: thesis: verum
end;
end;