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) ) }
proof
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;
{ 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 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;
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