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

for Q being Subset of A holds

( w in right-Lang Q iff w -succ_of (Q,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

for Q being Subset of A holds

( w in right-Lang Q iff w -succ_of (Q,A) meets the FinalS of A )

let F be Subset of (E ^omega); :: thesis: for A being non empty automaton over F

for Q being Subset of A holds

( w in right-Lang Q iff w -succ_of (Q,A) meets the FinalS of A )

let A be non empty automaton over F; :: thesis: for Q being Subset of A holds

( w in right-Lang Q iff w -succ_of (Q,A) meets the FinalS of A )

let Q be Subset of A; :: thesis: ( w in right-Lang Q iff w -succ_of (Q,A) meets the FinalS of A )

thus ( w in right-Lang Q implies w -succ_of (Q,A) meets the FinalS of A ) :: thesis: ( w -succ_of (Q,A) meets the FinalS of A implies w in right-Lang Q )

for F being Subset of (E ^omega)

for A being non empty automaton over F

for Q being Subset of A holds

( w in right-Lang Q iff w -succ_of (Q,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

for Q being Subset of A holds

( w in right-Lang Q iff w -succ_of (Q,A) meets the FinalS of A )

let F be Subset of (E ^omega); :: thesis: for A being non empty automaton over F

for Q being Subset of A holds

( w in right-Lang Q iff w -succ_of (Q,A) meets the FinalS of A )

let A be non empty automaton over F; :: thesis: for Q being Subset of A holds

( w in right-Lang Q iff w -succ_of (Q,A) meets the FinalS of A )

let Q be Subset of A; :: thesis: ( w in right-Lang Q iff w -succ_of (Q,A) meets the FinalS of A )

thus ( w in right-Lang Q implies w -succ_of (Q,A) meets the FinalS of A ) :: thesis: ( w -succ_of (Q,A) meets the FinalS of A implies w in right-Lang Q )

proof

thus
( w -succ_of (Q,A) meets the FinalS of A implies w in right-Lang Q )
; :: thesis: verum
assume
w in right-Lang Q
; :: thesis: w -succ_of (Q,A) meets the FinalS of A

then ex w9 being Element of E ^omega st

( w = w9 & w9 -succ_of (Q,A) meets the FinalS of A ) ;

hence w -succ_of (Q,A) meets the FinalS of A ; :: thesis: verum

end;then ex w9 being Element of E ^omega st

( w = w9 & w9 -succ_of (Q,A) meets the FinalS of A ) ;

hence w -succ_of (Q,A) meets the FinalS of A ; :: thesis: verum