let a, b be Point of R^1 ; :: according to TOPALG_2:def 3 :: thesis: ( not a in R^1 A or not b in R^1 A or [.a,b.] c= R^1 A )
R^1 A = A by TOPREALB:def 3;
hence ( not a in R^1 A or not b in R^1 A or [.a,b.] c= R^1 A ) by JCT_MISC:def 1; :: thesis: verum