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

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