:: deftheorem Def9 defines Set_Union OPENLATT:def 9 :
for L being D_Lattice
for b₂ being BinOp of (StoneS L) holds
( b₂ = Set_Union L iff for A, B being Element of StoneS L holds b₂ . (A,B) = A \/ B );