let T, T2 be complete lower TopLattice; ( T2 is TopAugmentation of [:T,T:] implies for f being Function of T2,T st f = inf_op T holds
f is continuous )
assume A1:
RelStr(# the carrier of T2, the InternalRel of T2 #) = RelStr(# the carrier of [:T,T:], the InternalRel of [:T,T:] #)
; YELLOW_9:def 4 for f being Function of T2,T st f = inf_op T holds
f is continuous
let f be Function of T2,T; ( f = inf_op T implies f is continuous )
assume A2:
f = inf_op T
; f is continuous
f is infs-preserving
proof
let X be
Subset of
T2;
WAYBEL_0:def 32 f preserves_inf_of X
reconsider Y =
X as
Subset of
[:T,T:] by A1;
assume A3:
ex_inf_of X,
T2
;
WAYBEL_0:def 30 ( ex_inf_of f .: X,T & "/\" ((f .: X),T) = f . ("/\" (X,T2)) )
thus
ex_inf_of f .: X,
T
by YELLOW_0:17;
"/\" ((f .: X),T) = f . ("/\" (X,T2))
A4:
inf_op T preserves_inf_of Y
by WAYBEL_0:def 32;
ex_inf_of Y,
[:T,T:]
by A3, A1, YELLOW_0:14;
hence
inf (f .: X) = f . (inf X)
by A1, A2, A4, YELLOW_0:27;
verum
end;
hence
f is continuous
by Th9; verum