theorem :: FILTER_2:83

for L being Lattice
for p being Element of L st L is C_Lattice & L is modular holds
latt (L,(.p.>) is C_Lattice