set A = { (Line (x1,x2)) where x1, x2 is Element of REAL n : verum } ;
{ (Line (x1,x2)) where x1, x2 is Element of REAL n : verum } c= bool (REAL n)
proof
let L be object ; :: according to TARSKI:def 3 :: thesis: ( not L in { (Line (x1,x2)) where x1, x2 is Element of REAL n : verum } or L in bool (REAL n) )
assume L in { (Line (x1,x2)) where x1, x2 is Element of REAL n : verum } ; :: thesis: L in bool (REAL n)
then ex x1, x2 being Element of REAL n st L = Line (x1,x2) ;
hence L in bool (REAL n) ; :: thesis: verum
end;
hence { (Line (x1,x2)) where x1, x2 is Element of REAL n : verum } is Subset-Family of (REAL n) ; :: thesis: verum