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

proof

let x be set ; :: 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