let N be with_infima topological_semilattice TopPoset; for C being Subset of N st subrelstr C is meet-inheriting holds
subrelstr (Cl C) is meet-inheriting
let C be Subset of N; ( subrelstr C is meet-inheriting implies subrelstr (Cl C) is meet-inheriting )
assume A1:
subrelstr C is meet-inheriting
; subrelstr (Cl C) is meet-inheriting
set A = Cl C;
set S = subrelstr (Cl C);
let x, y be Element of N; YELLOW_0:def 16 ( not x in the carrier of (subrelstr (Cl C)) or not y in the carrier of (subrelstr (Cl C)) or not ex_inf_of {x,y},N or "/\" ({x,y},N) in the carrier of (subrelstr (Cl C)) )
assume that
A2:
x in the carrier of (subrelstr (Cl C))
and
A3:
y in the carrier of (subrelstr (Cl C))
and
ex_inf_of {x,y},N
; "/\" ({x,y},N) in the carrier of (subrelstr (Cl C))
A4:
the carrier of (subrelstr (Cl C)) = Cl C
by YELLOW_0:def 15;
for V being a_neighborhood of x "/\" y holds V meets C
proof
set NN =
[:N,N:];
let V be
a_neighborhood of
x "/\" y;
V meets C
A5:
the
carrier of
[:N,N:] = [: the carrier of N, the carrier of N:]
by BORSUK_1:def 2;
then reconsider xy =
[x,y] as
Point of
[:N,N:] by YELLOW_3:def 2;
the
carrier of
[:N,N:] = [: the carrier of N, the carrier of N:]
by YELLOW_3:def 2;
then reconsider f =
inf_op N as
Function of
[:N,N:],
N by A5;
A6:
f . xy =
f . (
x,
y)
.=
x "/\" y
by WAYBEL_2:def 4
;
f is
continuous
by YELLOW13:def 5;
then consider H being
a_neighborhood of
xy such that A7:
f .: H c= V
by A6, BORSUK_1:def 1;
consider A being
Subset-Family of
[:N,N:] such that A8:
Int H = union A
and A9:
for
e being
set st
e in A holds
ex
X1,
Y1 being
Subset of
N st
(
e = [:X1,Y1:] &
X1 is
open &
Y1 is
open )
by BORSUK_1:5;
xy in union A
by A8, CONNSP_2:def 1;
then consider K being
set such that A10:
xy in K
and A11:
K in A
by TARSKI:def 4;
consider Ix,
Iy being
Subset of
N such that A12:
K = [:Ix,Iy:]
and A13:
Ix is
open
and A14:
Iy is
open
by A9, A11;
A15:
x in Ix
by A10, A12, ZFMISC_1:87;
A16:
y in Iy
by A10, A12, ZFMISC_1:87;
A17:
Ix = Int Ix
by A13, TOPS_1:23;
Iy = Int Iy
by A14, TOPS_1:23;
then reconsider Iy =
Iy as
a_neighborhood of
y by A16, CONNSP_2:def 1;
Iy meets C
by A3, A4, CONNSP_2:27;
then consider iy being
object such that A18:
iy in Iy
and A19:
iy in C
by XBOOLE_0:3;
reconsider Ix =
Ix as
a_neighborhood of
x by A15, A17, CONNSP_2:def 1;
Ix meets C
by A2, A4, CONNSP_2:27;
then consider ix being
object such that A20:
ix in Ix
and A21:
ix in C
by XBOOLE_0:3;
reconsider ix =
ix,
iy =
iy as
Element of
N by A20, A18;
now ex a being Element of the carrier of N st
( a in V & a in C )
[ix,iy] in K
by A12, A20, A18, ZFMISC_1:87;
then A22:
[ix,iy] in Int H
by A8, A11, TARSKI:def 4;
take a =
ix "/\" iy;
( a in V & a in C )A23:
dom f = the
carrier of
[:N,N:]
by FUNCT_2:def 1;
A24:
Int H c= H
by TOPS_1:16;
f . (
ix,
iy)
= ix "/\" iy
by WAYBEL_2:def 4;
then
ix "/\" iy in f .: H
by A24, A23, A22, FUNCT_1:def 6;
hence
a in V
by A7;
a in CA25:
ex_inf_of {ix,iy},
N
by YELLOW_0:21;
the
carrier of
(subrelstr C) = C
by YELLOW_0:def 15;
then
inf {ix,iy} in C
by A25, A1, A21, A19;
hence
a in C
by YELLOW_0:40;
verum end;
hence
V meets C
by XBOOLE_0:3;
verum
end;
then
x "/\" y in Cl C
by CONNSP_2:27;
hence
"/\" ({x,y},N) in the carrier of (subrelstr (Cl C))
by A4, YELLOW_0:40; verum