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;