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 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 (E ^omega)
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 (E ^omega); :: 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 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 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 A4, REWRITE3:103;
hence w in Lang A by A5; :: thesis: verum