let x1, x2 be set ; :: thesis: for X being finite set st x1 <> x2 holds
card (Choose (X,0,x1,x2)) = 1
let X be finite set ; :: thesis: ( x1 <> x2 implies card (Choose (X,0,x1,x2)) = 1 )
assume A1: x1 <> x2 ; :: thesis: card (Choose (X,0,x1,x2)) = 1

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

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

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

proof

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

end;

( Empty " {x1} = {} & card {} = 0 ) by FUNCT_1:72, RELAT_1:38;
then Empty in Choose (X,0,x1,x2) by Def1;
then Choose (X,0,x1,x2) = {Empty} by A4, ZFMISC_1:33;
hence card (Choose (X,0,x1,x2)) = 1 by CARD_1:30; :: thesis: verum

end;

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

then consider f being Function such that
A7: dom f = X and
A8: rng f = {x2} by FUNCT_1:5;
rng f c= {x1,x2} by A8, ZFMISC_1:36;
then A9: f is Function of X,{x1,x2} by A7, FUNCT_2:2;
A10: Choose (X,0,x1,x2) c= {f}

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Choose (X,0,x1,x2) or z in {f} )
assume z in Choose (X,0,x1,x2) ; :: thesis: z in {f}
then consider g being Function of X,{x1,x2} such that
A11: z = g and
A12: card (g " {x1}) = 0 by Def1;
g " {x1} = {} by A12;
then not x1 in rng g by FUNCT_1:72;
then ( not rng g = {x1} & not rng g = {x1,x2} ) by TARSKI:def 1, TARSKI:def 2;
then ( dom g = X & rng g = {x2} ) by A6, FUNCT_2:def 1, ZFMISC_1:36;
then g = f by A7, A8, FUNCT_1:7;
hence z in {f} by A11, TARSKI:def 1; :: thesis: verum

end;

not x1 in rng f by A1, A8, TARSKI:def 1;
then A13: f " {x1} = {} by FUNCT_1:72;
card {} = 0 ;
then f in Choose (X,0,x1,x2) by A13, A9, Def1;
then Choose (X,0,x1,x2) = {f} by A10, ZFMISC_1:33;
hence card (Choose (X,0,x1,x2)) = 1 by CARD_1:30; :: thesis: verum

end;

end;