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 set holds
( x in the_subsets_of_card X,Y iff x = Y )

proof

let x be set ; :: 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 X' being Subset of Y such that
A2: ( X' = x & card X' = X ) ;
reconsider X' = X' as finite Subset of Y ;
card (Y \ X') = (card Y) - (card X') by CARD_2:63
.= 0 by A2, A1 ;
then Y \ X' = {} ;
then Y c= X' by XBOOLE_1:37;
hence x = Y by A2, XBOOLE_0:def 10; :: thesis: verum

end;

assume A3: x = Y ; :: thesis: x in the_subsets_of_card X,Y
then x c= Y ;
then reconsider x' = x as Subset of Y ;
x' in the_subsets_of_card X,Y by A1, A3;
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