S \/ (S ~) = (((S ~) ~) \/ (S ~)) ~ by RELAT_1:23
.= (S \/ (S ~)) ~ ;
hence S \/ (S ~) is symmetric by RELAT_2:13; :: thesis: verum