theorem :: FILTER_1:48

for L1, L2 being Lattice holds [:L1,L2:] .: = [:(L1 .:),(L2 .:):] ;