the Object-Kind of (SCM R) = SCM-OK R by Def1;
then reconsider S = s as SCM-State of R by PBOOLE:155;
S . a in the carrier of R ;
hence s . a is Element of R ; :: thesis: verum