let E be set ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( s in Lang w,S iff w ==>* s,S )
thus ( s in Lang w,S implies w ==>* s,S ) :: thesis: ( w ==>* s,S implies s in Lang w,S )

proof

assume s in Lang w,S ; :: thesis: w ==>* s,S
then ex t being Element of E ^omega st
( t = s & w ==>* t,S ) ;
hence w ==>* s,S ; :: thesis: verum

end;

thus ( w ==>* s,S implies s in Lang w,S ) ; :: thesis: verum