consider v, w being Point of V such that
A1: v <> w by STRUCT_0:def 10;
take L = Line (v,w); :: thesis: ( not L is trivial & L is being_line )
thus not L is trivial :: thesis: L is being_line
proof
take v ; :: according to ZFMISC_1:def 10 :: thesis: ex b1 being object st
( v in L & b1 in L & not v = b1 )
take w ; :: thesis: ( v in L & w in L & not v = w )
thus ( v in L & w in L ) by Th72; :: thesis: not v = w
thus v <> w by A1; :: thesis: verum
end;
take v ; :: according to RLTOPSP1:def 15 :: thesis: ex x2 being Element of V st L = Line (v,x2)
take w ; :: thesis: L = Line (v,w)
thus L = Line (v,w) ; :: thesis: verum