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