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 )

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

hence
the_subsets_of_card (X,Y) = {Y}
by TARSKI:def 1; :: thesis: verum
let x be object ; :: thesis: ( x in the_subsets_of_card (X,Y) iff x = Y )

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;hereby :: thesis: ( x = Y implies x in the_subsets_of_card (X,Y) )

reconsider xx = x as set by TARSKI:1;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;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

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