let L be Lattice; :: thesis: for D1, D2 being non empty Subset of L holds D1 "\/" D2 = D2 "\/" D1
let D1, D2 be non empty Subset of L; :: thesis: D1 "\/" D2 = D2 "\/" D1
let r be Element of L; :: according to FILTER_2:def 1 :: thesis: ( r in D1 "\/" D2 iff r in D2 "\/" D1 )
thus ( r in D1 "\/" D2 implies r in D2 "\/" D1 ) :: thesis: ( r in D2 "\/" D1 implies r in D1 "\/" D2 )

proof

assume r in D1 "\/" D2 ; :: thesis: r in D2 "\/" D1
then ex p, q being Element of L st
( r = p "\/" q & p in D1 & q in D2 ) ;
hence r in D2 "\/" D1 ; :: thesis: verum

end;

assume r in D2 "\/" D1 ; :: thesis: r in D1 "\/" D2
then ex p, q being Element of L st
( r = p "\/" q & p in D2 & q in D1 ) ;
hence r in D1 "\/" D2 ; :: thesis: verum