let E be set ; :: thesis: for S, T, U being semi-Thue-system of E
for w being Element of E ^omega st S,T are_equivalent_wrt w & S c= U & U c= T holds
( S,U are_equivalent_wrt w & U,T are_equivalent_wrt w )
let S, T, U be semi-Thue-system of E; :: thesis: for w being Element of E ^omega st S,T are_equivalent_wrt w & S c= U & U c= T holds
( S,U are_equivalent_wrt w & U,T are_equivalent_wrt w )
let w be Element of E ^omega ; :: thesis: ( S,T are_equivalent_wrt w & S c= U & U c= T implies ( S,U are_equivalent_wrt w & U,T are_equivalent_wrt w ) )
assume that
A1: Lang w,S = Lang w,T and
A2: ( S c= U & U c= T ) ; :: according to REWRITE2:def 9 :: thesis: ( S,U are_equivalent_wrt w & U,T are_equivalent_wrt w )
( Lang w,S c= Lang w,U & Lang w,U c= Lang w,T ) by A2, Th48;
hence Lang w,S = Lang w,U by A1, XBOOLE_0:def 10; :: according to REWRITE2:def 9 :: thesis: U,T are_equivalent_wrt w
hence U,T are_equivalent_wrt w by A1, Def9; :: thesis: verum