set S = the semi-Thue-system of E;
take the semi-Thue-system of E \/ ( the semi-Thue-system of E ~) ; :: thesis: the semi-Thue-system of E \/ ( the semi-Thue-system of E ~) is symmetric
thus the semi-Thue-system of E \/ ( the semi-Thue-system of E ~) is symmetric ; :: thesis: verum