set Y = { B where B is Subset of X : ( card B = (card A) + 1 & A c= B ) } ;
{ B where B is Subset of X : ( card B = (card A) + 1 & A c= B ) } c= bool X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { B where B is Subset of X : ( card B = (card A) + 1 & A c= B ) } or x in bool X )
assume x in { B where B is Subset of X : ( card B = (card A) + 1 & A c= B ) } ; :: thesis: x in bool X
then ex B1 being Subset of X st
( x = B1 & card B1 = (card A) + 1 & A c= B1 ) ;
hence x in bool X ; :: thesis: verum

end;

hence { B where B is Subset of X : ( card B = (card A) + 1 & A c= B ) } is Subset of (bool X) ; :: thesis: verum