let x1, x2 be set ; :: thesis: for X being finite set
for k being Nat st card X < k holds
Choose (X,k,x1,x2) is empty
let X be finite set ; :: thesis: for k being Nat st card X < k holds
Choose (X,k,x1,x2) is empty
let k be Nat; :: 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 set such that
A2: z in Choose (X,k,x1,x2) by XBOOLE_0:def 1;
ex f being Function of X,{x1,x2} st
( f = z & card (f " {x1}) = k ) by A2, Def1;
hence contradiction by A1, NAT_1:44; :: thesis: verum