let L be Lattice; :: thesis: for D1, D2 being non empty Subset of holds D1 "\/" D2 = D2 "\/" D1
let D1, D2 be non empty Subset of ; :: thesis: D1 "\/" D2 = D2 "\/" D1
let r be Element of ; :: 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 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 st
( r = p "\/" q & p in D2 & q in D1 ) ;
hence r in D1 "\/" D2 ; :: thesis: verum