let s be State of SCM+FSA ; :: thesis: dom (s | Int-Locations ) = Int-Locations
Int-Locations c= dom s by Th69;
hence dom (s | Int-Locations ) = Int-Locations by RELAT_1:91; :: thesis: verum