reconsider S = s as SCM-State of by Def1;
S . a in the carrier of R ;
hence s . a is Element of ; :: thesis: verum