let X be non empty finite set ; :: thesis: for P being a_partition of X st card P < card X holds
ex p being set ex x, y being object 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 being set ex x, y being object st
( p in P & x in p & y in p & x <> y ) )
assume A1: card P < card X ; :: thesis: ex p being set ex x, y being object st
( p in P & x in p & y in p & x <> y )
A2: card P in Segm (card X) by A1, NAT_1:44;
consider x, y being object such that
A3: x in X and
A4: y in X and
A5: x <> y and
A6: (proj P) . x = (proj P) . y by A2, FINSEQ_4:65;
take p = (proj P) . x; :: thesis: ex x, y being object st
( p in P & x in p & y in p & x <> y )
take x ; :: thesis: ex y being object 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 A3, FUNCT_2:5; :: thesis: ( x in p & y in p & x <> y )
thus ( x in p & y in p ) by A3, A4, A6, EQREL_1:def 9; :: thesis: x <> y
thus x <> y by A5; :: thesis: verum