theorem LemY: :: SRINGS_4:14

for X being set
for S being with_empty_element Subset-Family of X holds DIFFERENCE (S,S) = { (A \ B) where A, B is Element of S : verum }