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:
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
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 ;
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 ;
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 ;
A15: x in Ix by ;
A16: y in Iy by ;
A17: Ix = Int Ix by ;
Iy = Int Iy by ;
then reconsider Iy = Iy as a_neighborhood of y by ;
Iy meets C by ;
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 ;
Ix meets C by ;
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 ;
now :: thesis: ex a being Element of the carrier of N st
( a in V & a in C )
[ix,iy] in K by ;
then A22: [ix,iy] in Int H by ;
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 ;
hence a in V by A7; :: thesis: a in C
A25: ex_inf_of {ix,iy},N by YELLOW_0:21;
the carrier of () = 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;
hence V meets C by XBOOLE_0:3; :: thesis: verum
end;
then x "/\" y in Cl C by CONNSP_2:27;
hence "/\" ({x,y},N) in the carrier of (subrelstr (Cl C)) by ; :: thesis: verum