theorem :: SUBSET_1:13

for E being set
for A, B being Subset of E holds A \ B = A /\ (B `)