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

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

proof

hence
{ B where B is Subset of X : ( card B = (card A) + 1 & A c= B ) } is Subset of (bool X)
; :: thesis: verum
let x be object ; :: 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;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