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