let N be with_infima topological_semilattice TopPoset; :: thesis: 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; :: thesis: ( subrelstr C is meet-inheriting implies subrelstr (Cl C) is meet-inheriting )
assume A1:
subrelstr C is meet-inheriting
; :: thesis: subrelstr (Cl C) is meet-inheriting
set A = Cl C;
set S = subrelstr (Cl C);
let x, y be Element of N; :: according to YELLOW_0:def 16 :: thesis: ( 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 A2:
( x in the carrier of (subrelstr (Cl C)) & y in the carrier of (subrelstr (Cl C)) & ex_inf_of {x,y},N )
; :: thesis: "/\" {x,y},N in the carrier of (subrelstr (Cl C))
A3:
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
let V be
a_neighborhood of
x "/\" y;
:: thesis: V meets C
set NN =
[:N,N:];
A4:
the
carrier of
[:N,N:] = [:the carrier of N,the carrier of N:]
by BORSUK_1:def 5;
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 A4;
A5:
f is
continuous
by YELLOW13:def 5;
reconsider xy =
[x,y] as
Point of
[:N,N:] by A4, YELLOW_3:def 2;
f . xy =
f . x,
y
.=
x "/\" y
by WAYBEL_2:def 4
;
then consider H being
a_neighborhood of
xy such that A6:
f .: H c= V
by A5, BORSUK_1:def 3;
consider A being
Subset-Family of
[:N,N:] such that A7:
Int H = union A
and A8:
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:45;
xy in union A
by A7, CONNSP_2:def 1;
then consider K being
set such that A9:
xy in K
and A10:
K in A
by TARSKI:def 4;
consider Ix,
Iy being
Subset of
N such that A11:
(
K = [:Ix,Iy:] &
Ix is
open &
Iy is
open )
by A8, A10;
(
x in Ix &
Ix = Int Ix )
by A9, A11, TOPS_1:55, ZFMISC_1:106;
then reconsider Ix =
Ix as
a_neighborhood of
x by CONNSP_2:def 1;
Ix meets C
by A2, A3, CONNSP_2:34;
then consider ix being
set such that A12:
(
ix in Ix &
ix in C )
by XBOOLE_0:3;
(
y in Iy &
Iy = Int Iy )
by A9, A11, TOPS_1:55, ZFMISC_1:106;
then reconsider Iy =
Iy as
a_neighborhood of
y by CONNSP_2:def 1;
Iy meets C
by A2, A3, CONNSP_2:34;
then consider iy being
set such that A13:
(
iy in Iy &
iy in C )
by XBOOLE_0:3;
reconsider ix =
ix,
iy =
iy as
Element of
N by A12, A13;
now take a =
ix "/\" iy;
:: thesis: ( a in V & a in C )A14:
f . ix,
iy = ix "/\" iy
by WAYBEL_2:def 4;
A15:
dom f = the
carrier of
[:N,N:]
by FUNCT_2:def 1;
[ix,iy] in K
by A11, A12, A13, ZFMISC_1:106;
then A16:
[ix,iy] in Int H
by A7, A10, TARSKI:def 4;
Int H c= H
by TOPS_1:44;
then
ix "/\" iy in f .: H
by A14, A15, A16, FUNCT_1:def 12;
hence
a in V
by A6;
:: thesis: a in CA17:
the
carrier of
(subrelstr C) = C
by YELLOW_0:def 15;
ex_inf_of {ix,iy},
N
by YELLOW_0:21;
then
inf {ix,iy} in C
by A1, A12, A13, A17, YELLOW_0:def 16;
hence
a in C
by YELLOW_0:40;
:: thesis: verum end;
hence
V meets C
by XBOOLE_0:3;
:: thesis: verum
end;
then
x "/\" y in Cl C
by CONNSP_2:34;
hence
"/\" {x,y},N in the carrier of (subrelstr (Cl C))
by A3, YELLOW_0:40; :: thesis: verum