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
thus for x being set st x in Lang w,S holds
x in Lang w,T :: according to TARSKI:def 3 :: thesis: verum

proof

let x be set ; :: thesis: ( x in Lang w,S implies 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

end;