theorem Th20: :: SURREALR:20

for X1, X2 being set holds -- (X1 \/ X2) = (-- X1) \/ (-- X2)