let X be set ; :: thesis: for P being finite a_partition of X
for S being Subset of X holds
( ( for p being set st p in P holds
p meets S ) iff card (P | S) = card P )
let P be finite a_partition of X; :: thesis: for S being Subset of X holds
( ( for p being set st p in P holds
p meets S ) iff card (P | S) = card P )
let S be Subset of X; :: thesis: ( ( for p being set st p in P holds
p meets S ) iff card (P | S) = card P )

per cases ( X = {} or X <> {} ) ;

suppose A1: X = {} ; :: thesis: ( ( for p being set st p in P holds
p meets S ) iff card (P | S) = card P )

hereby :: thesis: ( card (P | S) = card P implies for p being set st p in P holds
p meets S )

assume for p being set st p in P holds
p meets S ; :: thesis: card (P | S) = card P
S = {} by A1;
hence card (P | S) = {} by CARD_1:27, EQREL_1:32
.= card P by A1, CARD_1:27, EQREL_1:32 ;
:: thesis: verum

end;

thus ( card (P | S) = card P implies for p being set st p in P holds
p meets S ) by A1, EQREL_1:32; :: thesis: verum

end;

suppose A2: X <> {} ; :: thesis: ( ( for p being set st p in P holds
p meets S ) iff card (P | S) = card P )

set PS = P | S;
reconsider Pp1 = P as non empty finite set by A2;

hereby :: thesis: ( card (P | S) = card P implies for p being set st p in P holds
p meets S )

assume A3: for p being set st p in P holds
p meets S ; :: thesis: card (P | S) = card P
set p = the Element of P;
the Element of P in Pp1 ;
then the Element of P meets S by A3;
then the Element of P /\ S in P | S ;
then reconsider PSp1 = P | S as non empty finite set ;
defpred S₁[ set , set ] means ( $1 in P & $2 = $1 /\ S );
A4: for x being set st x in P holds
ex y being set st
( y in PSp1 & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in P implies ex y being set st
( y in PSp1 & S₁[x,y] ) )
assume A5: x in P ; :: thesis: ex y being set st
( y in PSp1 & S₁[x,y] )
take x /\ S ; :: thesis: ( x /\ S in PSp1 & S₁[x,x /\ S] )
x meets S by A5, A3;
hence ( x /\ S in PSp1 & S₁[x,x /\ S] ) by A5; :: thesis: verum

end;

consider f being Function of P,PSp1 such that
A6: for x being set st x in P holds
S₁[x,f . x] from FUNCT_2:sch 1(A4);

now

let x1, x2 be set ; :: thesis: ( x1 in P & x2 in P & f . x1 = f . x2 implies x1 = x2 )
assume that
A7: x1 in P and
A8: x2 in P and
A9: f . x1 = f . x2 ; :: thesis: x1 = x2
A10: f . x1 = x1 /\ S by A7, A6;
A11: f . x2 = x2 /\ S by A8, A6;
x1 meets S by A7, A3;
then f . x1 in P | S by A10, A7;
then f . x1 <> {} by EQREL_1:def 4;
then consider x being set such that
A12: x in f . x1 by XBOOLE_0:def 1;
( x in x1 & x in x2 ) by A12, A9, A10, A11, XBOOLE_0:def 4;
then x1 meets x2 by XBOOLE_0:3;
hence x1 = x2 by A7, A8, EQREL_1:def 4; :: thesis: verum

end;

then A13: f is one-to-one by FUNCT_2:19;
rng f = PSp1

proof

thus rng f c= PSp1 :: according to XBOOLE_0:def 10 :: thesis: PSp1 c= rng f

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in PSp1 )
assume y in rng f ; :: thesis: y in PSp1
then consider x being set such that
A14: x in P and
A15: f . x = y by FUNCT_2:11;
x meets S by A3, A14;
then x /\ S in P | S by A14;
hence y in PSp1 by A15, A14, A6; :: thesis: verum

end;

thus PSp1 c= rng f :: thesis: verum

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in PSp1 or y in rng f )
assume y in PSp1 ; :: thesis: y in rng f
then consider p being Element of P such that
A16: y = p /\ S and
p meets S ;
A17: p in Pp1 ;
then f . p = p /\ S by A6;
hence y in rng f by A16, A17, FUNCT_2:4; :: thesis: verum

end;

end;

then f is onto by FUNCT_2:def 3;
hence card (P | S) = card P by A13, EULER_1:11; :: thesis: verum

end;

assume A18: card (P | S) = card P ; :: thesis: for p being set st p in P holds
p meets S
defpred S₁[ set , set ] means ( $1 in P | S & $2 in Pp1 & $1 = $2 /\ S );
A19: for x being set st x in P | S holds
ex y being set st
( y in Pp1 & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in P | S implies ex y being set st
( y in Pp1 & S₁[x,y] ) )
assume A20: x in P | S ; :: thesis: ex y being set st
( y in Pp1 & S₁[x,y] )
then consider p being Element of P such that
A21: x = p /\ S and
p meets S ;
take p ; :: thesis: ( p in Pp1 & S₁[x,p] )
thus ( p in Pp1 & S₁[x,p] ) by A20, A21; :: thesis: verum

end;

consider f being Function of (P | S),Pp1 such that
A22: for x being set st x in P | S holds
S₁[x,f . x] from FUNCT_2:sch 1(A19);
A23: f is one-to-one

proof

let x1, x2 be set ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A24: x1 in dom f and
A25: x2 in dom f and
A26: f . x1 = f . x2 ; :: thesis: x1 = x2
x1 = (f . x1) /\ S by A24, A22;
hence x1 = x2 by A26, A25, A22; :: thesis: verum

end;

A27: rng f = P by A18, A23, FINSEQ_4:63;
let p be set ; :: thesis: ( p in P implies p meets S )
assume p in P ; :: thesis: p meets S
then consider ps being set such that
A28: ps in dom f and
A29: p = f . ps by A27, FUNCT_1:def 3;
A30: dom f = P | S by FUNCT_2:def 1;
A31: ps = p /\ S by A29, A28, A22;
not ps is empty by A28, A30, EQREL_1:def 4;
then ex x being set st x in ps by XBOOLE_0:def 1;
hence p meets S by A31, XBOOLE_0:4; :: thesis: verum

end;

end;