let X be set ; :: thesis: the_subsets_of_card (0,X) = {0}
for x being object holds
( x in the_subsets_of_card (0,X) iff x = 0 )

proof

let x be object ; :: thesis: ( x in the_subsets_of_card (0,X) iff x = 0 )

hereby :: thesis: ( x = 0 implies x in the_subsets_of_card (0,X) )

assume x in the_subsets_of_card (0,X) ; :: thesis: x = 0
then ex x9 being Subset of X st
( x9 = x & card x9 = 0 ) ;
hence x = 0 ; :: thesis: verum

end;

assume A1: x = 0 ; :: thesis: x in the_subsets_of_card (0,X)
then reconsider x9 = x as Subset of X by XBOOLE_1:2;
card x9 = 0 by A1;
hence x in the_subsets_of_card (0,X) ; :: thesis: verum

end;

hence the_subsets_of_card (0,X) = {0} by TARSKI:def 1; :: thesis: verum