let E be set ; :: thesis: for S, T being semi-Thue-system of E st S c= T holds

==>.-relation S c= ==>.-relation T

let S, T be semi-Thue-system of E; :: thesis: ( S c= T implies ==>.-relation S c= ==>.-relation T )

assume A1: S c= T ; :: thesis: ==>.-relation S c= ==>.-relation T

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ==>.-relation S or x in ==>.-relation T )

assume A2: x in ==>.-relation S ; :: thesis: x in ==>.-relation T

then consider s, t being object such that

A3: x = [s,t] and

A4: ( s in E ^omega & t in E ^omega ) by RELSET_1:2;

reconsider s = s, t = t as Element of E ^omega by A4;

s ==>. t,S by A2, A3, Def6;

then s ==>. t,T by A1, Th19;

hence x in ==>.-relation T by A3, Def6; :: thesis: verum

==>.-relation S c= ==>.-relation T

let S, T be semi-Thue-system of E; :: thesis: ( S c= T implies ==>.-relation S c= ==>.-relation T )

assume A1: S c= T ; :: thesis: ==>.-relation S c= ==>.-relation T

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ==>.-relation S or x in ==>.-relation T )

assume A2: x in ==>.-relation S ; :: thesis: x in ==>.-relation T

then consider s, t being object such that

A3: x = [s,t] and

A4: ( s in E ^omega & t in E ^omega ) by RELSET_1:2;

reconsider s = s, t = t as Element of E ^omega by A4;

s ==>. t,S by A2, A3, Def6;

then s ==>. t,T by A1, Th19;

hence x in ==>.-relation T by A3, Def6; :: thesis: verum