let S be Hausdorff TopLattice; ( ( for N being net of S st N is eventually-directed holds
( ex_sup_of N & sup N in Lim N ) ) & ( for x being Element of S holds x "/\" is continuous ) implies S is meet-continuous )
assume that
A1:
for N being net of S st N is eventually-directed holds
( ex_sup_of N & sup N in Lim N )
and
A2:
for x being Element of S holds x "/\" is continuous
; S is meet-continuous
for X being non empty directed Subset of S holds ex_sup_of X,S
proof
let X be non
empty directed Subset of
S;
ex_sup_of X,S
reconsider n =
id X as
Function of
X, the
carrier of
S by FUNCT_2:7;
set N =
NetStr(#
X,
( the InternalRel of S |_2 X),
n #);
NetStr(#
X,
( the InternalRel of S |_2 X),
n #) is
eventually-directed
by WAYBEL_2:20;
then A3:
ex_sup_of NetStr(#
X,
( the InternalRel of S |_2 X),
n #)
by A1;
rng the
mapping of
NetStr(#
X,
( the InternalRel of S |_2 X),
n #)
= X
by RELAT_1:45;
hence
ex_sup_of X,
S
by A3;
verum
end;
hence
S is up-complete
by WAYBEL_0:75; WAYBEL_2:def 7 S is satisfying_MC
for x being Element of S
for M being net of S st M is eventually-directed holds
x "/\" (sup M) = sup ({x} "/\" (rng (netmap (M,S))))
proof
let x be
Element of
S;
for M being net of S st M is eventually-directed holds
x "/\" (sup M) = sup ({x} "/\" (rng (netmap (M,S))))let M be
net of
S;
( M is eventually-directed implies x "/\" (sup M) = sup ({x} "/\" (rng (netmap (M,S)))) )
assume A4:
M is
eventually-directed
;
x "/\" (sup M) = sup ({x} "/\" (rng (netmap (M,S))))
A5:
sup M in Lim M
by A1, A4;
then reconsider M1 =
M as
convergent net of
S by YELLOW_6:def 16;
set xM =
x "/\" M;
x "/\" M is
eventually-directed
by A4, WAYBEL_2:27;
then A6:
sup (x "/\" M) in Lim (x "/\" M)
by A1;
x "/\" is
continuous
by A2;
then A7:
x "/\" (lim M1) in Lim (x "/\" M1)
by Th26;
reconsider xM =
x "/\" M as
convergent net of
S by A6, YELLOW_6:def 16;
thus x "/\" (sup M) =
x "/\" (lim M1)
by A5, YELLOW_6:def 17
.=
lim xM
by A7, YELLOW_6:def 17
.=
Sup
by A6, YELLOW_6:def 17
.=
sup (rng the mapping of xM)
by YELLOW_2:def 5
.=
sup ({x} "/\" (rng (netmap (M,S))))
by WAYBEL_2:23
;
verum
end;
hence
S is satisfying_MC
by Th9; verum