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 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 ; :: thesis: "/\" ({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

hence "/\" ({x,y},N) in the carrier of (subrelstr (Cl C)) by A4, YELLOW_0:40; :: thesis: verum

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 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 ; :: thesis: "/\" ({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

then
x "/\" y in Cl C
by CONNSP_2:27;
set NN = [:N,N:];

let V be a_neighborhood of x "/\" y; :: thesis: 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;

end;let V be a_neighborhood of x "/\" y; :: thesis: 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 :: thesis: ex a being Element of the carrier of N st

( a in V & a in C )

hence
V meets C
by XBOOLE_0:3; :: thesis: verum( 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; :: thesis: ( 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; :: thesis: a in C

A25: 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; :: thesis: verum

end;then A22: [ix,iy] in Int H by A8, A11, TARSKI:def 4;

take a = ix "/\" iy; :: thesis: ( 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; :: thesis: a in C

A25: 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; :: thesis: verum

hence "/\" ({x,y},N) in the carrier of (subrelstr (Cl C)) by A4, YELLOW_0:40; :: thesis: verum