:: deftheorem Def4 defines IntPrefSpace PREFER_1:def 7 :
for A being non empty set
for a, b being Element of A
for b₄ being strict PreferenceStr holds
( b₄ = IntPrefSpace (A,a,b) iff ( the carrier of b₄ = A & the PrefRel of b₄ = {} & the ToleranceRel of b₄ = {[a,a],[b,b]} & the InternalRel of b₄ = {[a,b],[b,a]} ) );