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