theorem :: YELLOW12:1

for A, X being set holds (delta X) .: A c= [:A,A:]