set X = { A where A is Subset of AS : A is being_line } ;
{ A where A is Subset of AS : A is being_line } c= bool the carrier of AS

proof

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

end;

hence { A where A is Subset of AS : A is being_line } is Subset-Family of AS ; :: thesis: verum