let E be set ; for S being semi-Thue-system of E
for s, w being Element of E ^omega holds
( s in Lang (w,S) iff w ==>* s,S )
let S be semi-Thue-system of E; for s, w being Element of E ^omega holds
( s in Lang (w,S) iff w ==>* s,S )
let s, w be Element of E ^omega ; ( s in Lang (w,S) iff w ==>* s,S )
thus
( s in Lang (w,S) implies w ==>* s,S )
( w ==>* s,S implies s in Lang (w,S) )
thus
( w ==>* s,S implies s in Lang (w,S) )
; verum