theorem Th84: :: FILTER_2:84

for L being Lattice
for p, q being Element of L st L is C_Lattice & L is modular & p [= q holds
latt (L,[#p,q#]) is C_Lattice