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 )

for x being object holds

( x in the_subsets_of_card (0,X) iff x = 0 )

proof

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

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

assume A1:
x = 0
; :: thesis: 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;then ex x9 being Subset of X st

( x9 = x & card x9 = 0 ) ;

hence x = 0 ; :: thesis: verum

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