:: deftheorem Def5 defines IdPrefSpace PREFER_1:def 5 :
for A being set
for b₂ being strict PreferenceStr holds
( b₂ = IdPrefSpace A iff ( the carrier of b₂ = A & the PrefRel of b₂ = {} & the ToleranceRel of b₂ = id A & the InternalRel of b₂ = {} ) );