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