theorem :: LATTICE2:68

for L being Lattice holds
( L is finite iff L .: is finite ) ;