theorem :: FILTER_2:18

for L being Lattice
for p, q being Element of L
for p9, q9 being Element of (L .:) holds
( p "/\" q = (p .:) "\/" (q .:) & p "\/" q = (p .:) "/\" (q .:) & p9 "/\" q9 = (.: p9) "\/" (.: q9) & p9 "\/" q9 = (.: p9) "/\" (.: q9) ) ;