let U be non empty set ; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum