let T, T2 be complete lower TopLattice; :: thesis: ( 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:] #) ; :: according to YELLOW_9:def 4 :: thesis: for f being Function of T2,T st f = inf_op T holds
f is continuous
let f be Function of T2,T; :: thesis: ( f = inf_op T implies f is continuous )
assume A2: f = inf_op T ; :: thesis: f is continuous
f is infs-preserving

proof

let X be Subset of T2; :: according to WAYBEL_0:def 32 :: thesis: f preserves_inf_of X
reconsider Y = X as Subset of [:T,T:] by A1;
assume A3: ex_inf_of X,T2 ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of f .: X,T & "/\" ((f .: X),T) = f . ("/\" (X,T2)) )
thus ex_inf_of f .: X,T by YELLOW_0:17; :: thesis: "/\" ((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; :: thesis: verum

end;

hence f is continuous by Th9; :: thesis: verum