theorem :: FILTER_2:19

for L being Lattice
for p, q being Element of L
for p9, q9 being Element of (L .:) holds
( ( p [= q implies q .: [= p .: ) & ( q .: [= p .: implies p [= q ) & ( p9 [= q9 implies .: q9 [= .: p9 ) & ( .: q9 [= .: p9 implies p9 [= q9 ) ) by LATTICE2:38, LATTICE2:39;