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:
2 c= card (A . i) by A2, NAT_1:40;
then reconsider Ai = A . i as non trivial finite set by PENCIL_1:4;
consider x, y being set such that
A3: x in Ai and
A4: y in Ai and
A5: x <> y by REALSET1:14;
A6: i in dom A by A2, CARD_1:47, FUNCT_1:def 4;
assume A7: for z being set st z in A . i holds
not Cut A,i,z is Hall ; :: thesis:
then not Cut A,i,x is Hall by A3;
then consider JJ1 being finite set such that
A8: ( JJ1 c= dom (Cut A,i,x) & card JJ1 > card (union (Cut A,i,x),JJ1) ) by Def4;
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:5
.= (card JJ1) - 1 by CARD_1:50 ;
union (Cut A,i,x),JJ1 = (union A,(JJ1 \ {i})) \/ ((A . i) \ {x}) by A8, A9, Th14;
then A11: card (JJ1 \ {i}) >= card ((union A,(JJ1 \ {i})) \/ ((A . i) \ {x})) by A8, A10, SPPOL_1:6;
A12: JJ1 \ {i} c= dom (Cut A,i,x) by A8, XBOOLE_1:1;
{i} misses JJ1 \ {i} by XBOOLE_1:79;
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, A12, ZFMISC_1:54; :: thesis:

end;

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

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

end;

then consider J1 being finite set such that
A15: not i in J1 and
A16: ( J1 c= dom (Cut A,i,x) & card J1 >= card ((union A,J1) \/ ((A . i) \ {x})) ) ;
set S1 = (union A,J1) \/ ((A . i) \ {x});
not Cut A,i,y is Hall by A4, A7;
then consider JJ2 being finite set such that
A17: ( JJ2 c= dom (Cut A,i,y) & card JJ2 > card (union (Cut A,i,y),JJ2) ) by Def4;
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 A18: i in JJ2 ; :: thesis:

set J2 = JJ2 \ {i};
A19: card (JJ2 \ {i}) = (card JJ2) - (card {i}) by A18, EULER_1:5
.= (card JJ2) - 1 by CARD_1:50 ;
union (Cut A,i,y),JJ2 = (union A,(JJ2 \ {i})) \/ ((A . i) \ {y}) by A17, A18, Th14;
then A20: card (JJ2 \ {i}) >= card ((union A,(JJ2 \ {i})) \/ ((A . i) \ {y})) by A17, A19, SPPOL_1:6;
A21: JJ2 \ {i} c= dom (Cut A,i,y) by A17, XBOOLE_1:1;
{i} misses JJ2 \ {i} by XBOOLE_1:79;
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 A20, A21, ZFMISC_1:54; :: 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 A17, 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, Def4; :: thesis:

end;

then consider J2 being finite set such that
A24: not i in J2 and
A25: ( J2 c= dom (Cut A,i,y) & card J2 >= card ((union A,J2) \/ ((A . i) \ {y})) ) ;
set S2 = (union A,J2) \/ ((A . i) \ {y});
(card J1) + (card J2) >= (card ((union A,J1) \/ ((A . i) \ {x}))) + (card ((union A,J2) \/ ((A . i) \ {y}))) by A16, A25, XREAL_1:9;
then A26: (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 \/ J2)) \/ Ai c= ((union A,J1) \/ (Ai \ {x})) \/ ((union A,J2) \/ (Ai \ {y}))

proof

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

per cases by A27, XBOOLE_0:def 3;

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

then consider j being set such that
A28: ( j in J1 \/ J2 & j in dom A & a in A . j ) by Def1;
( ( j in J1 or j in J2 ) & j in dom A & a in A . j ) by A28, XBOOLE_0:def 3;
then ( a in union A,J1 or a in union A,J2 ) by 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 union A,{i} by A6, Th5;
then consider j being set such that
A29: ( j in {i} & j in dom A & a in A . j ) by Def1;
( a in union A,{i} or a in union A,J1 or a in union A,J2 ) by A29, Def1;
then ( a in Ai or a in union A,J1 or a in union A,J2 ) by A6, Th5;
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 A30: card (((union A,J1) \/ (Ai \ {x})) \/ ((union A,J2) \/ (Ai \ {y}))) >= card ((union A,(J1 \/ J2)) \/ Ai) by NAT_1:44;
(union A,J1) /\ (union A,J2) c= ((union A,J1) \/ (Ai \ {x})) /\ ((union A,J2) \/ (Ai \ {y}))

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in (union A,J1) /\ (union A,J2) ; :: thesis:
then A31: ( a in union A,J1 & a in union A,J2 ) by XBOOLE_0:def 4;
then consider j being set such that
A32: ( j in J1 & j in dom A & a in A . j ) by Def1;
consider k being set such that
A33: ( k in J2 & k in dom A & a in A . k ) by A31, Def1;
( a in union A,J1 or a in Ai \ {x} ) by A32, Def1;
then A34: a in (union A,J1) \/ (Ai \ {x}) by XBOOLE_0:def 3;
( a in union A,J2 or a in Ai \ {y} ) by A33, Def1;
then a in (union A,J2) \/ (Ai \ {y}) by XBOOLE_0:def 3;
hence a in ((union A,J1) \/ (Ai \ {x})) /\ ((union A,J2) \/ (Ai \ {y})) by A34, 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:44;
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 A30, XREAL_1:9;
then A35: (card J1) + (card J2) >= (card ((union A,(J1 \/ J2)) \/ Ai)) + (card ((union A,J1) /\ (union A,J2))) by A26, XXREAL_0:2;
union A,(J1 /\ J2) c= (union A,J1) /\ (union A,J2)

proof

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

end;

then card ((union A,J1) /\ (union A,J2)) >= card (union A,(J1 /\ J2)) by NAT_1:44;
then (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:9;
then A37: (card J1) + (card J2) >= (card (Ai \/ (union A,(J1 \/ J2)))) + (card (union A,(J1 /\ J2))) by A35, XXREAL_0:2;
A38: J1 /\ J2 c= J1 by XBOOLE_1:17;
J1 c= dom A by A16, Def2;
then J1 /\ J2 c= dom A by A38, XBOOLE_1:1;
then A39: card (union A,(J1 /\ J2)) >= card (J1 /\ J2) by A1, Def4;
A40: ( J1 c= dom A & J2 c= dom A ) by A16, A25, Def2;
A41: not i in J1 \/ J2 by A15, A24, XBOOLE_0:def 3;
reconsider L = {i} \/ (J1 \/ J2) as finite set ;
( {i} c= dom A & J1 \/ J2 c= dom A ) by A6, A40, XBOOLE_1:8, ZFMISC_1:37;
then L c= dom A by XBOOLE_1:8;
then card (union A,({i} \/ (J1 \/ J2))) >= card ({i} \/ (J1 \/ J2)) by A1, Def4;
then A42: card (union A,(({i} \/ J1) \/ J2)) >= card ({i} \/ (J1 \/ J2)) by XBOOLE_1:4;
A43: card (union A,(({i} \/ J1) \/ J2)) = card (Ai \/ (union A,(J1 \/ J2))) by A6, Th9;
card ({i} \/ (J1 \/ J2)) = (card {i}) + (card (J1 \/ J2)) by A41, CARD_2:53, ZFMISC_1:56;
then card (Ai \/ (union A,(J1 \/ J2))) >= 1 + (card (J1 \/ J2)) by A42, A43, CARD_1:50;
then A44: (card (Ai \/ (union A,(J1 \/ J2)))) + (card (union A,(J1 /\ J2))) >= (1 + (card (J1 \/ J2))) + (card (J1 /\ J2)) by A39, XREAL_1:9;
(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 A37, A44, NAT_1:13; :: thesis: