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 of 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 of 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 of 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 of 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 w' being Element of E ^omega st
( w' = w & Q meets w' -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