for X being set
for S being Field_Subset of X
for A, B being set st A in S & B in S holds
A \ B in S by FINSUB_1:def 3;