let U be non empty set ; for A1, A2, B1, B2 being Subset of U st A1 c= A2 & B1 c= B2 holds
DIFFERENCE ((Inter (A1,A2)),(Inter (B1,B2))) = { C where C is Subset of U : ( A1 \ B2 c= C & C c= A2 \ B1 ) }
let A1, A2, B1, B2 be Subset of U; ( A1 c= A2 & B1 c= B2 implies DIFFERENCE ((Inter (A1,A2)),(Inter (B1,B2))) = { C where C is Subset of U : ( A1 \ B2 c= C & C c= A2 \ B1 ) } )
assume
( A1 c= A2 & B1 c= B2 )
; DIFFERENCE ((Inter (A1,A2)),(Inter (B1,B2))) = { C where C is Subset of U : ( A1 \ B2 c= C & C c= A2 \ B1 ) }
then reconsider A12 = Inter (A1,A2), B12 = Inter (B1,B2) as non empty ordered Subset-Family of U by Th25;
A1:
( min A12 = A1 & max A12 = A2 )
by Th27;
( min B12 = B1 & max B12 = B2 )
by Th27;
hence
DIFFERENCE ((Inter (A1,A2)),(Inter (B1,B2))) = { C where C is Subset of U : ( A1 \ B2 c= C & C c= A2 \ B1 ) }
by Th38, A1; verum