let IAlph be non empty set ; :: thesis: for fsm being non empty FSM over IAlph
for q being State of fsm holds <*q*> is_admissible_for <*> IAlph
let fsm be non empty FSM over IAlph; :: thesis: for q being State of fsm holds <*q*> is_admissible_for <*> IAlph
let q be State of fsm; :: thesis: <*q*> is_admissible_for <*> IAlph
( (q,(<*> IAlph)) -admissible = <*q*> & q = <*q*> . 1 ) by Th1;
hence <*q*> is_admissible_for <*> IAlph ; :: thesis: verum