let X, Y be finite set ; :: thesis: ( card Y = X implies the_subsets_of_card (X,Y) = {Y} )
assume A1: card Y = X ; :: thesis: the_subsets_of_card (X,Y) = {Y}
for x being object holds
( x in the_subsets_of_card (X,Y) iff x = Y )
proof
let x be object ; :: thesis: ( x in the_subsets_of_card (X,Y) iff x = Y )
hereby :: thesis: ( x = Y implies x in the_subsets_of_card (X,Y) )
assume x in the_subsets_of_card (X,Y) ; :: thesis: x = Y
then consider X9 being Subset of Y such that
A2: X9 = x and
A3: card X9 = X ;
reconsider X9 = X9 as finite Subset of Y ;
card (Y \ X9) = (card Y) - (card X9) by CARD_2:44
.= 0 by A1, A3 ;
then Y \ X9 = {} ;
then Y c= X9 by XBOOLE_1:37;
hence x = Y by A2, XBOOLE_0:def 10; :: thesis: verum
end;
reconsider xx = x as set by TARSKI:1;
assume A4: x = Y ; :: thesis: x in the_subsets_of_card (X,Y)
then xx c= Y ;
then reconsider x9 = x as Subset of Y ;
x9 in the_subsets_of_card (X,Y) by A1, A4;
hence x in the_subsets_of_card (X,Y) ; :: thesis: verum
end;
hence the_subsets_of_card (X,Y) = {Y} by TARSKI:def 1; :: thesis: verum