set B = { A where A is Subset of T : A is condensed } ;
{ A where A is Subset of T : A is condensed } c= bool the carrier of T

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { A where A is Subset of T : A is condensed } or x in bool the carrier of T )
assume x in { A where A is Subset of T : A is condensed } ; :: thesis: x in bool the carrier of T
then ex A being Subset of T st
( x = A & A is condensed ) ;
hence x in bool the carrier of T ; :: thesis: verum

end;

hence { A where A is Subset of T : A is condensed } is Subset-Family of T ; :: thesis: verum