let X be finite set ; :: thesis: for k being Nat
for x1, x2 being object st card X < k holds
Choose (X,k,x1,x2) is empty
let k be Nat; :: thesis: for x1, x2 being object st card X < k holds
Choose (X,k,x1,x2) is empty
let x1, x2 be object ; :: thesis: ( card X < k implies Choose (X,k,x1,x2) is empty )
assume A1: card X < k ; :: thesis: Choose (X,k,x1,x2) is empty
assume not Choose (X,k,x1,x2) is empty ; :: thesis: contradiction
then consider z being object such that
A2: z in Choose (X,k,x1,x2) ;
ex f being Function of X,{x1,x2} st
( f = z & card (f " {x1}) = k ) by A2, Def1;
hence contradiction by A1, NAT_1:43; :: thesis: verum