:: deftheorem defsp defines spanning REALALG1:def 8 :
for L being non empty addLoopStr
for S being Subset of L holds
( S is spanning iff S \/ (- S) = the carrier of L );