let X be non empty finite set ; :: thesis: for P being a_partition of X st card P < card X holds
ex p, x, y being set st
( p in P & x in p & y in p & x <> y )
let P be a_partition of X; :: thesis: ( card P < card X implies ex p, x, y being set st
( p in P & x in p & y in p & x <> y ) )
assume A: card P < card X ; :: thesis: ex p, x, y being set st
( p in P & x in p & y in p & x <> y )
Aa: card P in card X by A, NAT_1:44;
consider x, y being set such that
C: x in X and
D: y in X and
E: x <> y and
F: (proj P) . x = (proj P) . y by Aa, FINSEQ_4:65;
take p = (proj P) . x; :: thesis: ex x, y being set st
( p in P & x in p & y in p & x <> y )
take x ; :: thesis: ex y being set st
( p in P & x in p & y in p & x <> y )
take y ; :: thesis: ( p in P & x in p & y in p & x <> y )
thus p in P by C, FUNCT_2:5; :: thesis: ( x in p & y in p & x <> y )
thus ( x in p & y in p ) by C, D, F, EQREL_1:def 9; :: thesis: x <> y
thus x <> y by E; :: thesis: verum