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) )

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

thus
( w ==>* s,S implies s in Lang (w,S) )
; :: thesis: verum
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;then ex t being Element of E ^omega st

( t = s & w ==>* t,S ) ;

hence w ==>* s,S ; :: thesis: verum