let T be Hausdorff TopLattice; :: thesis: for N being convergent net of T
for x being Element of T st x "/\" is continuous holds
x "/\" (lim N) in Lim (x "/\" N)
let N be convergent net of T; :: thesis: for x being Element of T st x "/\" is continuous holds
x "/\" (lim N) in Lim (x "/\" N)
let x be Element of T; :: thesis: ( x "/\" is continuous implies x "/\" (lim N) in Lim (x "/\" N) )
assume A1: x "/\" is continuous ; :: thesis: x "/\" (lim N) in Lim (x "/\" N)
x "/\" (lim N) = (x "/\") . (lim N) by WAYBEL_1:def 18;
then x "/\" (lim N) in Lim ((x "/\") * N) by A1, Th25;
hence x "/\" (lim N) in Lim (x "/\" N) by Th18; :: thesis: verum