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 consider x' being Subset of X such that
A1: ( x' = x & card x' = 0 ) ;
thus x = 0 by A1; :: thesis: verum

end;

assume A2: x = 0 ; :: thesis: x in the_subsets_of_card 0 ,X
then reconsider x' = x as Subset of X by XBOOLE_1:2;
card x' = 0 by A2;
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