:: deftheorem Def3 defines | FINTOPO6:def 3 :
for T being non empty RelStr
for P being non empty Subset of T
for b₃ being non empty strict SubSpace of T holds
( b₃ = T | P iff [#] b₃ = P );