let x1, x2 be set ; :: thesis: for X being finite set holds card (Choose X,(card X),x1,x2) = 1
let X be finite set ; :: thesis: card (Choose X,(card X),x1,x2) = 1

per cases ( X is empty or not X is empty ) ;

suppose A1: X is empty ; :: thesis: card (Choose X,(card X),x1,x2) = 1

A2: rng {} = {} ;
dom {} = X by A1;
then reconsider Empty = {} as Function of X,{x1,x2} by A2, FUNCT_2:4, XBOOLE_1:2;
A3: Choose X,(card X),x1,x2 c= {Empty}

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Choose X,(card X),x1,x2 or z in {Empty} )
assume z in Choose X,(card X),x1,x2 ; :: thesis: z in {Empty}
then consider f being Function of X,{x1,x2} such that
A4: z = f and
card (f " {x1}) = card X by Def1;
dom f = X by FUNCT_2:def 1;
then f = Empty ;
hence z in {Empty} by A4, TARSKI:def 1; :: thesis: verum

end;

Empty " {x1} = {} by FUNCT_1:142, RELAT_1:60;
then Empty in Choose X,(card X),x1,x2 by A1, Def1;
then Choose X,(card X),x1,x2 = {Empty} by A3, ZFMISC_1:39;
hence card (Choose X,(card X),x1,x2) = 1 by CARD_1:50; :: thesis: verum

end;

suppose A5: not X is empty ; :: thesis: card (Choose X,(card X),x1,x2) = 1

then consider f being Function such that
A6: dom f = X and
A7: rng f = {x1} by FUNCT_1:15;
rng f c= {x1,x2} by A7, ZFMISC_1:42;
then A8: f is Function of X,{x1,x2} by A6, FUNCT_2:4;
A9: Choose X,(card X),x1,x2 c= {f}

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Choose X,(card X),x1,x2 or z in {f} )
assume z in Choose X,(card X),x1,x2 ; :: thesis: z in {f}
then consider g being Function of X,{x1,x2} such that
A10: z = g and
A11: card (g " {x1}) = card X by Def1;

A12: now

per cases ( x1 = x2 or x1 <> x2 ) ;

suppose x1 = x2 ; :: thesis: rng g = {x1}

then {x1,x2} = {x1} by ENUMSET1:69;
hence rng g = {x1} by A5, ZFMISC_1:39; :: thesis: verum

end;

suppose A13: x1 <> x2 ; :: thesis: rng g = {x1}

g " {x2} = {}

proof

assume g " {x2} <> {} ; :: thesis: contradiction
then consider z being set such that
A14: z in g " {x2} by XBOOLE_0:def 1;
g . z in {x2} by A14, FUNCT_1:def 13;
then A15: g . z = x2 by TARSKI:def 1;
g " {x1} = X by A11, Th1;
then g . z in {x1} by A14, FUNCT_1:def 13;
hence contradiction by A13, A15, TARSKI:def 1; :: thesis: verum

end;

then not x2 in rng g by FUNCT_1:142;
then ( not rng g = {x2} & not rng g = {x1,x2} ) by TARSKI:def 1, TARSKI:def 2;
hence rng g = {x1} by A5, ZFMISC_1:42; :: thesis: verum

end;

end;

end;

dom g = X by FUNCT_2:def 1;
then g = f by A6, A7, A12, FUNCT_1:17;
hence z in {f} by A10, TARSKI:def 1; :: thesis: verum

end;

card (f " {x1}) = card X by A6, A7, RELAT_1:169;
then f in Choose X,(card X),x1,x2 by A8, Def1;
then Choose X,(card X),x1,x2 = {f} by A9, ZFMISC_1:39;
hence card (Choose X,(card X),x1,x2) = 1 by CARD_1:50; :: thesis: verum

end;

end;