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;

A1: DIFFERENCE (A,B) c= { 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;

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

proof

{ C where C is Subset of U : ( (min A) \ (max B) c= C & C c= (max A) \ (min B) ) } c= DIFFERENCE (A,B)
let x be object ; :: 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 A2: 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

A3: ( Y in A & Z in B & x = Y \ Z ) by SETFAM_1:def 6;

DIFFERENCE (A,B) is Subset-Family of U by Th37;

then reconsider x = x as Subset of U by A2;

( min A c= Y & Y c= max A & min B c= Z & Z c= max B ) by A3, Th28;

then ( (min A) \ (max B) c= x & x c= (max A) \ (min B) ) by A3, XBOOLE_1:35;

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;assume A2: 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

A3: ( Y in A & Z in B & x = Y \ Z ) by SETFAM_1:def 6;

DIFFERENCE (A,B) is Subset-Family of U by Th37;

then reconsider x = x as Subset of U by A2;

( min A c= Y & Y c= max A & min B c= Z & Z c= max B ) by A3, Th28;

then ( (min A) \ (max B) c= x & x c= (max A) \ (min B) ) by A3, XBOOLE_1:35;

hence x in { C where C is Subset of U : ( (min A) \ (max B) c= C & C c= (max A) \ (min B) ) } ; :: thesis: verum

proof

hence
DIFFERENCE (A,B) = { C where C is Subset of U : ( (min A) \ (max B) c= C & C c= (max A) \ (min B) ) }
by A1; :: thesis: verum
let x be object ; :: 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

A4: ( 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 Lm2;

then A5: (max B) ` c= (min B) ` by SUBSET_1:12;

(x9 \/ ((max B) `)) /\ ((min B) `) = (x9 /\ ((min B) `)) \/ (((max B) `) /\ ((min B) `)) by XBOOLE_1:23

.= (x9 /\ ((min B) `)) \/ ((max B) `) by A5, XBOOLE_1:28 ;

then A6: (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 A7: ( ((x9 \/ ((max B) `)) /\ ((min B) `)) ` c= ((max B) `) ` & ((min B) `) ` c= ((x9 \/ ((max B) `)) /\ ((min B) `)) ` ) by A6, SUBSET_1:12;

(x9 \/ (min A)) /\ (max A) = (x9 /\ (max A)) \/ ((min A) /\ (max A)) by XBOOLE_1:23

.= (x9 /\ (max A)) \/ (min A) by SETFAM_1:2, XBOOLE_1:28 ;

then ( min A c= (x9 \/ (min A)) /\ (max A) & (x9 \/ (min A)) /\ (max A) c= max A ) by XBOOLE_1:7, XBOOLE_1:17;

then A8: ( (x9 \/ (min A)) /\ (max A) in A & ((x9 \/ ((max B) `)) /\ ((min B) `)) ` in B ) by Th28, A7;

A9: (x9 \/ ((min A) \ (max B))) /\ ((max A) \ (min B)) = x9 /\ ((max A) \ (min B)) by A4, XBOOLE_1:12

.= x9 by A4, 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:13

.= (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:13

.= ((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 A9, SUBSET_1:13 ;

hence x in DIFFERENCE (A,B) by A4, A8, SETFAM_1:def 6; :: thesis: verum

end;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

A4: ( 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 Lm2;

then A5: (max B) ` c= (min B) ` by SUBSET_1:12;

(x9 \/ ((max B) `)) /\ ((min B) `) = (x9 /\ ((min B) `)) \/ (((max B) `) /\ ((min B) `)) by XBOOLE_1:23

.= (x9 /\ ((min B) `)) \/ ((max B) `) by A5, XBOOLE_1:28 ;

then A6: (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 A7: ( ((x9 \/ ((max B) `)) /\ ((min B) `)) ` c= ((max B) `) ` & ((min B) `) ` c= ((x9 \/ ((max B) `)) /\ ((min B) `)) ` ) by A6, SUBSET_1:12;

(x9 \/ (min A)) /\ (max A) = (x9 /\ (max A)) \/ ((min A) /\ (max A)) by XBOOLE_1:23

.= (x9 /\ (max A)) \/ (min A) by SETFAM_1:2, XBOOLE_1:28 ;

then ( min A c= (x9 \/ (min A)) /\ (max A) & (x9 \/ (min A)) /\ (max A) c= max A ) by XBOOLE_1:7, XBOOLE_1:17;

then A8: ( (x9 \/ (min A)) /\ (max A) in A & ((x9 \/ ((max B) `)) /\ ((min B) `)) ` in B ) by Th28, A7;

A9: (x9 \/ ((min A) \ (max B))) /\ ((max A) \ (min B)) = x9 /\ ((max A) \ (min B)) by A4, XBOOLE_1:12

.= x9 by A4, 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:13

.= (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:13

.= ((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 A9, SUBSET_1:13 ;

hence x in DIFFERENCE (A,B) by A4, A8, SETFAM_1:def 6; :: thesis: verum