theorem :: FILTER_2:47

for L being Lattice
for D1, D2 being non empty Subset of L holds D1 "\/" D2 = D2 "\/" D1