theorem :: FILTER_2:71

for L being Lattice holds
( latt (L,(.L.>) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & latt (L,<.L.)) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) )