let E be set ; :: thesis: for S, T being semi-Thue-system of E
for w, s being Element of E ^omega st S,T are_equivalent_wrt w & w ==>* s,S \/ T holds
w ==>* s,S
let S, T be semi-Thue-system of E; :: thesis: for w, s being Element of E ^omega st S,T are_equivalent_wrt w & w ==>* s,S \/ T holds
w ==>* s,S
let w, s be Element of E ^omega ; :: thesis: ( S,T are_equivalent_wrt w & w ==>* s,S \/ T implies w ==>* s,S )
assume that
A1: S,T are_equivalent_wrt w and
A2: w ==>* s,S \/ T ; :: thesis: w ==>* s,S
==>.-relation (S \/ T) reduces w,s by A2, Def7;
then ==>.-relation S reduces w,s by A1, Th58;
hence w ==>* s,S by Def7; :: thesis: verum