:: deftheorem defines semidiff SRINGS_4:def 1 :
for X being set
for S being with_empty_element Subset-Family of X holds semidiff S = DIFFERENCE (S,S);