let F be finite set ; :: thesis:
let A be FinSequence of bool F; :: thesis:
assume A1: A is Hall ; :: thesis:
let i be Element of NAT ; :: thesis:
assume A2: card (A . i) >= 2 ; :: thesis:
Segm 2 c= Segm (card (A . i)) by A2, NAT_1:39;
then reconsider Ai = A . i as non trivial finite set by PENCIL_1:4;
consider x, y being object such that
A3: x in Ai and
A4: y in Ai and
A5: x <> y by ZFMISC_1:def 10;
assume A6: for z being set st z in A . i holds
not Cut (A,i,z) is Hall ; :: thesis:
reconsider x = x, y = y as set by TARSKI:1;
not Cut (A,i,x) is Hall by A3, A6;
then consider JJ1 being finite set such that
A7: JJ1 c= dom (Cut (A,i,x)) and
A8: card JJ1 > card (union ((Cut (A,i,x)),JJ1)) ;
ex J1 being finite set st
( not i in J1 & J1 c= dom (Cut (A,i,x)) & card J1 >= card ((union (A,J1)) \/ ((A . i) \ {x})) )

proof

per cases ;

suppose A9: i in JJ1 ; :: thesis:

set J1 = JJ1 \ {i};
A10: card (JJ1 \ {i}) = (card JJ1) - (card {i}) by A9, EULER_1:4
.= (card JJ1) - 1 by CARD_1:30 ;
A11: ( JJ1 \ {i} c= dom (Cut (A,i,x)) & {i} misses JJ1 \ {i} ) by A7, XBOOLE_1:79;
union ((Cut (A,i,x)),JJ1) = (union (A,(JJ1 \ {i}))) \/ ((A . i) \ {x}) by A7, A9, Th14;
then card (JJ1 \ {i}) >= card ((union (A,(JJ1 \ {i}))) \/ ((A . i) \ {x})) by A8, A10, SPPOL_1:1;
hence ex J1 being finite set st
( not i in J1 & J1 c= dom (Cut (A,i,x)) & card J1 >= card ((union (A,J1)) \/ ((A . i) \ {x})) ) by A11, ZFMISC_1:48; :: thesis:

end;

suppose A12: not i in JJ1 ; :: thesis:

take J1 = JJ1; :: thesis:
A13: J1 c= dom A by A7, Def2;
card J1 > card (union (A,J1)) by A8, A12, Th13;
hence ( not i in J1 & J1 c= dom (Cut (A,i,x)) & card J1 >= card ((union (A,J1)) \/ ((A . i) \ {x})) ) by A1, A13; :: thesis:

end;

then consider J1 being finite set such that
A14: not i in J1 and
A15: J1 c= dom (Cut (A,i,x)) and
A16: card J1 >= card ((union (A,J1)) \/ ((A . i) \ {x})) ;
not Cut (A,i,y) is Hall by A4, A6;
then consider JJ2 being finite set such that
A17: JJ2 c= dom (Cut (A,i,y)) and
A18: card JJ2 > card (union ((Cut (A,i,y)),JJ2)) ;
ex J2 being finite set st
( not i in J2 & J2 c= dom (Cut (A,i,y)) & card J2 >= card ((union (A,J2)) \/ ((A . i) \ {y})) )

proof

per cases ;

suppose A19: i in JJ2 ; :: thesis:

set J2 = JJ2 \ {i};
A20: card (JJ2 \ {i}) = (card JJ2) - (card {i}) by A19, EULER_1:4
.= (card JJ2) - 1 by CARD_1:30 ;
A21: ( JJ2 \ {i} c= dom (Cut (A,i,y)) & {i} misses JJ2 \ {i} ) by A17, XBOOLE_1:79;
union ((Cut (A,i,y)),JJ2) = (union (A,(JJ2 \ {i}))) \/ ((A . i) \ {y}) by A17, A19, Th14;
then card (JJ2 \ {i}) >= card ((union (A,(JJ2 \ {i}))) \/ ((A . i) \ {y})) by A18, A20, SPPOL_1:1;
hence ex J2 being finite set st
( not i in J2 & J2 c= dom (Cut (A,i,y)) & card J2 >= card ((union (A,J2)) \/ ((A . i) \ {y})) ) by A21, ZFMISC_1:48; :: thesis:

end;

suppose A22: not i in JJ2 ; :: thesis:

set J2 = JJ2;
take JJ2 ; :: thesis:
A23: JJ2 c= dom A by A17, Def2;
card JJ2 > card (union (A,JJ2)) by A18, A22, Th13;
hence ( not i in JJ2 & JJ2 c= dom (Cut (A,i,y)) & card JJ2 >= card ((union (A,JJ2)) \/ ((A . i) \ {y})) ) by A1, A23; :: thesis:

end;

then consider J2 being finite set such that
A24: not i in J2 and
A25: J2 c= dom (Cut (A,i,y)) and
A26: card J2 >= card ((union (A,J2)) \/ ((A . i) \ {y})) ;
reconsider L = {i} \/ (J1 \/ J2) as finite set ;
A27: J2 c= dom A by A25, Def2;
(union (A,(J1 \/ J2))) \/ Ai c= ((union (A,J1)) \/ (Ai \ {x})) \/ ((union (A,J2)) \/ (Ai \ {y}))

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume A28: a in (union (A,(J1 \/ J2))) \/ Ai ; :: thesis:

per cases by A28, XBOOLE_0:def 3;

suppose a in union (A,(J1 \/ J2)) ; :: thesis:

then consider j being set such that
A29: j in J1 \/ J2 and
A30: ( j in dom A & a in A . j ) by Def1;
( j in J1 or j in J2 ) by A29, XBOOLE_0:def 3;
then ( a in union (A,J1) or a in union (A,J2) ) by A30, Def1;
then a in (union (A,J1)) \/ (union (A,J2)) by XBOOLE_0:def 3;
then a in ((union (A,J1)) \/ (union (A,J2))) \/ ((Ai \ {x}) \/ (Ai \ {y})) by XBOOLE_0:def 3;
then a in (((union (A,J1)) \/ (union (A,J2))) \/ (Ai \ {x})) \/ (Ai \ {y}) by XBOOLE_1:4;
then a in (((union (A,J1)) \/ (Ai \ {x})) \/ (union (A,J2))) \/ (Ai \ {y}) by XBOOLE_1:4;
hence a in ((union (A,J1)) \/ (Ai \ {x})) \/ ((union (A,J2)) \/ (Ai \ {y})) by XBOOLE_1:4; :: thesis:

end;

suppose a in Ai ; :: thesis:

then ( a in (Ai \ {x}) \/ (Ai \ {y}) or a in union (A,J1) or a in union (A,J2) ) by A3, A4, A5, Th10;
then ( a in ((Ai \ {x}) \/ (Ai \ {y})) \/ (union (A,J1)) or a in union (A,J2) ) by XBOOLE_0:def 3;
then a in (((Ai \ {x}) \/ (Ai \ {y})) \/ (union (A,J1))) \/ (union (A,J2)) by XBOOLE_0:def 3;
then a in ((union (A,J1)) \/ (union (A,J2))) \/ ((Ai \ {x}) \/ (Ai \ {y})) by XBOOLE_1:4;
then a in (((union (A,J1)) \/ (union (A,J2))) \/ (Ai \ {x})) \/ (Ai \ {y}) by XBOOLE_1:4;
then a in (((union (A,J1)) \/ (Ai \ {x})) \/ (union (A,J2))) \/ (Ai \ {y}) by XBOOLE_1:4;
hence a in ((union (A,J1)) \/ (Ai \ {x})) \/ ((union (A,J2)) \/ (Ai \ {y})) by XBOOLE_1:4; :: thesis:

end;

then A31: card (((union (A,J1)) \/ (Ai \ {x})) \/ ((union (A,J2)) \/ (Ai \ {y}))) >= card ((union (A,(J1 \/ J2))) \/ Ai) by NAT_1:43;
union (A,(J1 /\ J2)) c= (union (A,J1)) /\ (union (A,J2))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in union (A,(J1 /\ J2)) ; :: thesis:
then consider j being set such that
A32: j in J1 /\ J2 and
A33: ( j in dom A & x in A . j ) by Def1;
j in J2 by A32, XBOOLE_0:def 4;
then A34: x in union (A,J2) by A33, Def1;
j in J1 by A32, XBOOLE_0:def 4;
then x in union (A,J1) by A33, Def1;
hence x in (union (A,J1)) /\ (union (A,J2)) by A34, XBOOLE_0:def 4; :: thesis:

end;

then card ((union (A,J1)) /\ (union (A,J2))) >= card (union (A,(J1 /\ J2))) by NAT_1:43;
then A35: (card ((union (A,(J1 \/ J2))) \/ Ai)) + (card ((union (A,J1)) /\ (union (A,J2)))) >= (card (Ai \/ (union (A,(J1 \/ J2))))) + (card (union (A,(J1 /\ J2)))) by XREAL_1:7;
J1 c= dom A by A15, Def2;
then A36: J1 \/ J2 c= dom A by A27, XBOOLE_1:8;
A37: i in dom A by A2, CARD_1:27, FUNCT_1:def 2;
then {i} c= dom A by ZFMISC_1:31;
then L c= dom A by A36, XBOOLE_1:8;
then card (union (A,({i} \/ (J1 \/ J2)))) >= card ({i} \/ (J1 \/ J2)) by A1;
then A38: card (union (A,(({i} \/ J1) \/ J2))) >= card ({i} \/ (J1 \/ J2)) by XBOOLE_1:4;
not i in J1 \/ J2 by A14, A24, XBOOLE_0:def 3;
then A39: card ({i} \/ (J1 \/ J2)) = (card {i}) + (card (J1 \/ J2)) by CARD_2:40, ZFMISC_1:50;
( J1 /\ J2 c= J1 & J1 c= dom A ) by A15, Def2, XBOOLE_1:17;
then J1 /\ J2 c= dom A ;
then A40: card (union (A,(J1 /\ J2))) >= card (J1 /\ J2) by A1;
set S2 = (union (A,J2)) \/ ((A . i) \ {y});
set S1 = (union (A,J1)) \/ ((A . i) \ {x});
(card J1) + (card J2) >= (card ((union (A,J1)) \/ ((A . i) \ {x}))) + (card ((union (A,J2)) \/ ((A . i) \ {y}))) by A16, A26, XREAL_1:7;
then A41: (card J1) + (card J2) >= (card (((union (A,J1)) \/ (Ai \ {x})) \/ ((union (A,J2)) \/ (Ai \ {y})))) + (card (((union (A,J1)) \/ (Ai \ {x})) /\ ((union (A,J2)) \/ (Ai \ {y})))) by Th1;
(union (A,J1)) /\ (union (A,J2)) c= ((union (A,J1)) \/ (Ai \ {x})) /\ ((union (A,J2)) \/ (Ai \ {y}))

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume A42: a in (union (A,J1)) /\ (union (A,J2)) ; :: thesis:
then a in union (A,J2) by XBOOLE_0:def 4;
then A43: a in (union (A,J2)) \/ (Ai \ {y}) by XBOOLE_0:def 3;
a in union (A,J1) by A42, XBOOLE_0:def 4;
then a in (union (A,J1)) \/ (Ai \ {x}) by XBOOLE_0:def 3;
hence a in ((union (A,J1)) \/ (Ai \ {x})) /\ ((union (A,J2)) \/ (Ai \ {y})) by A43, XBOOLE_0:def 4; :: thesis:

end;

then card (((union (A,J1)) \/ (Ai \ {x})) /\ ((union (A,J2)) \/ (Ai \ {y}))) >= card ((union (A,J1)) /\ (union (A,J2))) by NAT_1:43;
then (card (((union (A,J1)) \/ (Ai \ {x})) \/ ((union (A,J2)) \/ (Ai \ {y})))) + (card (((union (A,J1)) \/ (Ai \ {x})) /\ ((union (A,J2)) \/ (Ai \ {y})))) >= (card ((union (A,(J1 \/ J2))) \/ Ai)) + (card ((union (A,J1)) /\ (union (A,J2)))) by A31, XREAL_1:7;
then (card J1) + (card J2) >= (card ((union (A,(J1 \/ J2))) \/ Ai)) + (card ((union (A,J1)) /\ (union (A,J2)))) by A41, XXREAL_0:2;
then A44: (card J1) + (card J2) >= (card (Ai \/ (union (A,(J1 \/ J2))))) + (card (union (A,(J1 /\ J2)))) by A35, XXREAL_0:2;
card (union (A,(({i} \/ J1) \/ J2))) = card (Ai \/ (union (A,(J1 \/ J2)))) by A37, Th9;
then card (Ai \/ (union (A,(J1 \/ J2)))) >= 1 + (card (J1 \/ J2)) by A38, A39, CARD_1:30;
then A45: (card (Ai \/ (union (A,(J1 \/ J2))))) + (card (union (A,(J1 /\ J2)))) >= (1 + (card (J1 \/ J2))) + (card (J1 /\ J2)) by A40, XREAL_1:7;
(card (J1 \/ J2)) + (card (J1 /\ J2)) = (card J1) + (card J2) by Th1;
then (1 + (card (J1 \/ J2))) + (card (J1 /\ J2)) = 1 + ((card J1) + (card J2)) ;
hence contradiction by A44, A45, NAT_1:13; :: thesis: