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; :: thesis: verum