let X be set ; :: thesis: for P being finite a_partition of X
for S being Subset of X holds card (P | S) <= card P
let P be finite a_partition of X; :: thesis: for S being Subset of X holds card (P | S) <= card P
let S be Subset of X; :: thesis: card (P | S) <= card P

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

suppose X = {} ; :: thesis: card (P | S) <= card P

then S = {} ;
hence card (P | S) <= card P ; :: thesis: verum

end;

suppose X <> {} ; :: thesis: card (P | S) <= card P

then reconsider Pp1 = P as non empty finite set ;
defpred S₂[ set ] means $1 meets S;
deffunc H₁( set ) -> Element of bool X = $1 /\ S;
A3: P | S = { H₁(x) where x is Element of Pp1 : S₂[x] } ;
card (P | S) <= card Pp1 from DILWORTH:sch 1(A3);
hence card (P | S) <= card P ; :: thesis: verum

end;

end;