for x being set
for R being Ring holds
( x is Data-Location of R iff x in Data-Locations ) by Def1, AMI_2:def 16, AMI_3:27;