:: deftheorem Def1 defines Ort_CompSet RUSUB_7:def 1 :
for X being RealUnitarySpace
for M being Subset of X
for b₃ being non empty Subset of X holds
( b₃ = Ort_CompSet M iff for x being Point of X holds
( x in b₃ iff for y being Point of X st y in M holds
y .|. x = 0 ) );