let D1, D2 be Subset of L; :: thesis: D1 "\/" D2 = D2 "\/" D1
thus D1 "\/" D2 c= D2 "\/" D1 :: according to XBOOLE_0:def 10 :: thesis: D2 "\/" D1 c= D1 "\/" D2

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in D1 "\/" D2 or q in D2 "\/" D1 )
assume q in D1 "\/" D2 ; :: thesis: q in D2 "\/" D1
then ex x, y being Element of L st
( q = x "\/" y & x in D1 & y in D2 ) ;
hence q in D2 "\/" D1 ; :: thesis: verum

end;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in D2 "\/" D1 or q in D1 "\/" D2 )
assume q in D2 "\/" D1 ; :: thesis: q in D1 "\/" D2
then ex x, y being Element of L st
( q = x "\/" y & x in D2 & y in D1 ) ;
hence q in D1 "\/" D2 ; :: thesis: verum