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

proof

assume w in Lang A ; :: thesis: w -succ_of the InitS of A,A meets the FinalS of A
then consider p, q being Element of A such that
A1: p in the InitS of A and
A2: q in the FinalS of A and
A3: p,w ==>* q,A by ThLang5;
q in w -succ_of the InitS of A,A by A1, A3, REWRITE3:103;
hence w -succ_of the InitS of A,A meets the FinalS of A by A2, XBOOLE_0:3; :: thesis: verum

end;

assume w -succ_of the InitS of A,A meets the FinalS of A ; :: thesis: w in Lang A
then consider x being set such that
A1: x in w -succ_of the InitS of A,A and
A2: x in the FinalS of A by XBOOLE_0:3;
reconsider x = x as Element of A by A1;
consider p being Element of A such that
B: ( p in the InitS of A & p,w ==>* x,A ) by A1, REWRITE3:103;
thus w in Lang A by A2, B; :: thesis: verum