let U be non empty set ; :: thesis: for A, B being non empty ordered Subset-Family of U holds DIFFERENCE A,B = { C where C is Subset of U : ( (min A) \ (max B) c= C & C c= (max A) \ (min B) ) }
let A, B be non empty ordered Subset-Family of U; :: thesis: DIFFERENCE A,B = { C where C is Subset of U : ( (min A) \ (max B) c= C & C c= (max A) \ (min B) ) }
set A1 = min A;
set B1 = min B;
set A2 = max A;
set B2 = max B;
a0: DIFFERENCE A,B c= { C where C is Subset of U : ( (min A) \ (max B) c= C & C c= (max A) \ (min B) ) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in DIFFERENCE A,B or x in { C where C is Subset of U : ( (min A) \ (max B) c= C & C c= (max A) \ (min B) ) } )
assume b1: x in DIFFERENCE A,B ; :: thesis: x in { C where C is Subset of U : ( (min A) \ (max B) c= C & C c= (max A) \ (min B) ) }
then consider Y, Z being set such that
b2: ( Y in A & Z in B & x = Y \ Z ) by SETFAM_1:def 6;
DIFFERENCE A,B is Subset-Family of U by Diff1;
then reconsider x = x as Subset of U by b1;
( min A c= Y & Y c= max A & min B c= Z & Z c= max B ) by b2, Nowe1;
then ( (min A) \ (max B) c= x & x c= (max A) \ (min B) ) by XBOOLE_1:35, b2;
hence x in { C where C is Subset of U : ( (min A) \ (max B) c= C & C c= (max A) \ (min B) ) } ; :: thesis: verum

end;

{ C where C is Subset of U : ( (min A) \ (max B) c= C & C c= (max A) \ (min B) ) } c= DIFFERENCE A,B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { C where C is Subset of U : ( (min A) \ (max B) c= C & C c= (max A) \ (min B) ) } or x in DIFFERENCE A,B )
assume x in { C where C is Subset of U : ( (min A) \ (max B) c= C & C c= (max A) \ (min B) ) } ; :: thesis: x in DIFFERENCE A,B
then consider x9 being Subset of U such that
e0: ( x9 = x & (min A) \ (max B) c= x9 & x9 c= (max A) \ (min B) ) ;
set A1 = min A;
set A2 = max A;
set B1 = min B;
set B2 = max B;
set z1 = (x9 \/ (min A)) /\ (max A);
set z2 = ((x9 \/ ((max B) ` )) /\ ((min B) ` )) ` ;
min B c= max B by DefMi;
then F7: (max B) ` c= (min B) ` by SUBSET_1:31;
(x9 \/ ((max B) ` )) /\ ((min B) ` ) = (x9 /\ ((min B) ` )) \/ (((max B) ` ) /\ ((min B) ` )) by XBOOLE_1:23
.= (x9 /\ ((min B) ` )) \/ ((max B) ` ) by F7, XBOOLE_1:28 ;
then F6: (max B) ` c= (x9 \/ ((max B) ` )) /\ ((min B) ` ) by XBOOLE_1:7;
(x9 \/ ((max B) ` )) /\ ((min B) ` ) c= (min B) ` by XBOOLE_1:17;
then F5: ( ((x9 \/ ((max B) ` )) /\ ((min B) ` )) ` c= ((max B) ` ) ` & ((min B) ` ) ` c= ((x9 \/ ((max B) ` )) /\ ((min B) ` )) ` ) by F6, SUBSET_1:31;
(x9 \/ (min A)) /\ (max A) = (x9 /\ (max A)) \/ ((min A) /\ (max A)) by XBOOLE_1:23
.= (x9 /\ (max A)) \/ (min A) by SETFAM_1:3, XBOOLE_1:28 ;
then ( min A c= (x9 \/ (min A)) /\ (max A) & (x9 \/ (min A)) /\ (max A) c= max A ) by XBOOLE_1:17, XBOOLE_1:7;
then F3: ( (x9 \/ (min A)) /\ (max A) in A & ((x9 \/ ((max B) ` )) /\ ((min B) ` )) ` in B ) by Nowe1, F5;
F1: (x9 \/ ((min A) \ (max B))) /\ ((max A) \ (min B)) = x9 /\ ((max A) \ (min B)) by e0, XBOOLE_1:12
.= x9 by e0, XBOOLE_1:28 ;
((x9 \/ (min A)) /\ (max A)) \ (((x9 \/ ((max B) ` )) /\ ((min B) ` )) ` ) = ((x9 \/ (min A)) /\ (max A)) /\ ((((x9 \/ ((max B) ` )) /\ ((min B) ` )) ` ) ` ) by SUBSET_1:32
.= (x9 \/ (min A)) /\ ((max A) /\ ((x9 \/ ((max B) ` )) /\ ((min B) ` ))) by XBOOLE_1:16
.= (x9 \/ (min A)) /\ ((x9 \/ ((max B) ` )) /\ (((min B) ` ) /\ (max A))) by XBOOLE_1:16
.= (x9 \/ (min A)) /\ ((x9 \/ ((max B) ` )) /\ ((max A) \ (min B))) by SUBSET_1:32
.= ((x9 \/ (min A)) /\ (x9 \/ ((max B) ` ))) /\ ((max A) \ (min B)) by XBOOLE_1:16
.= (x9 \/ ((min A) /\ ((max B) ` ))) /\ ((max A) \ (min B)) by XBOOLE_1:24
.= x9 by F1, SUBSET_1:32 ;
hence x in DIFFERENCE A,B by SETFAM_1:def 6, e0, F3; :: thesis: verum

end;

hence DIFFERENCE A,B = { C where C is Subset of U : ( (min A) \ (max B) c= C & C c= (max A) \ (min B) ) } by a0, XBOOLE_0:def 10; :: thesis: verum