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 S2[ set ] means $1 meets S;
deffunc H1( set ) -> Element of bool X = $1 /\ S;
A3: P | S = { H1(x) where x is Element of Pp1 : S2[x] } ;
card (P | S) <= card Pp1 from DILWORTH:sch 1(A3);
hence card (P | S) <= card P ; :: thesis: verum
end;
end;