consider L being non empty trivial TopLattice;
take L ; :: thesis: ( L is lim-inf & L is continuous & L is complete )
thus ( L is lim-inf & L is continuous & L is complete ) ; :: thesis: verum