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

for w being Element of E ^omega st S c= T holds

Lang (w,S) c= Lang (w,T)

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

Lang (w,S) c= Lang (w,T)

let w be Element of E ^omega ; :: thesis: ( S c= T implies Lang (w,S) c= Lang (w,T) )

assume A1: S c= T ; :: thesis: Lang (w,S) c= Lang (w,T)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Lang (w,S) or x in Lang (w,T) )

assume A2: x in Lang (w,S) ; :: thesis: x in Lang (w,T)

then reconsider y = x as Element of E ^omega ;

w ==>* y,S by A2, Th46;

then w ==>* y,T by A1, Th40;

hence x in Lang (w,T) ; :: thesis: verum

for w being Element of E ^omega st S c= T holds

Lang (w,S) c= Lang (w,T)

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

Lang (w,S) c= Lang (w,T)

let w be Element of E ^omega ; :: thesis: ( S c= T implies Lang (w,S) c= Lang (w,T) )

assume A1: S c= T ; :: thesis: Lang (w,S) c= Lang (w,T)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Lang (w,S) or x in Lang (w,T) )

assume A2: x in Lang (w,S) ; :: thesis: x in Lang (w,T)

then reconsider y = x as Element of E ^omega ;

w ==>* y,S by A2, Th46;

then w ==>* y,T by A1, Th40;

hence x in Lang (w,T) ; :: thesis: verum