let E be non empty set ; :: thesis: for w being Element of E ^omega
for F being Subset of ()
for A being non empty automaton over 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 ()
for A being non empty automaton over 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 (); :: thesis: for A being non empty automaton over 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 over 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 Th18;
q in w -succ_of ( the InitS of A,A) by ;
hence w -succ_of ( the InitS of A,A) meets the FinalS of A by ; :: 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 object such that
A4: x in w -succ_of ( the InitS of A,A) and
A5: x in the FinalS of A by XBOOLE_0:3;
reconsider x = x as Element of A by A4;
ex p being Element of A st
( p in the InitS of A & p,w ==>* x,A ) by ;
hence w in Lang A by A5; :: thesis: verum