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 nowosc1;
a2: ( min A12 = A1 & max A12 = A2 ) by nowosc2;
( min B12 = B1 & max B12 = B2 ) by nowosc2;
hence DIFFERENCE (Inter A1,A2),(Inter B1,B2) = { C where C is Subset of U : ( A1 \ B2 c= C & C c= A2 \ B1 ) } by LemmaC0, a2; :: thesis: verum