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

( 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