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