let x be set ; :: thesis: for R being good Ring holds
( x is Data-Location of R iff x in Data-Locations (SCM R) )
let R be good Ring; :: thesis: ( x is Data-Location of R iff x in Data-Locations (SCM R) )
Data-Locations (SCM R) = Data-Locations SCM by Th31;
hence ( x is Data-Location of R iff x in Data-Locations (SCM R) ) by Th1; :: thesis: verum