let E be non empty set ; :: thesis: for w being Element of E ^omega
for F being Subset of (E ^omega)
for SA being non empty semiautomaton over F
for Q being Subset of SA holds
( w in left-Lang Q iff Q meets w -succ_of ( the InitS of SA,SA) )
let w be Element of E ^omega ; :: thesis: for F being Subset of (E ^omega)
for SA being non empty semiautomaton over F
for Q being Subset of SA holds
( w in left-Lang Q iff Q meets w -succ_of ( the InitS of SA,SA) )
let F be Subset of (E ^omega); :: thesis: for SA being non empty semiautomaton over F
for Q being Subset of SA holds
( w in left-Lang Q iff Q meets w -succ_of ( the InitS of SA,SA) )
let SA be non empty semiautomaton over F; :: thesis: for Q being Subset of SA holds
( w in left-Lang Q iff Q meets w -succ_of ( the InitS of SA,SA) )
let Q be Subset of SA; :: thesis: ( w in left-Lang Q iff Q meets w -succ_of ( the InitS of SA,SA) )
thus ( w in left-Lang Q implies Q meets w -succ_of ( the InitS of SA,SA) ) :: thesis: ( Q meets w -succ_of ( the InitS of SA,SA) implies w in left-Lang Q )

proof

assume w in left-Lang Q ; :: thesis: Q meets w -succ_of ( the InitS of SA,SA)
then ex w9 being Element of E ^omega st
( w9 = w & Q meets w9 -succ_of ( the InitS of SA,SA) ) ;
hence Q meets w -succ_of ( the InitS of SA,SA) ; :: thesis: verum

end;

thus ( Q meets w -succ_of ( the InitS of SA,SA) implies w in left-Lang Q ) ; :: thesis: verum