let V be non trivial RealLinearSpace; :: thesis: for L being non trivial line of V ex p, q being Point of V st
( p <> q & L = Line (p,q) )
let L be non trivial line of V; :: thesis: ex p, q being Point of V st
( p <> q & L = Line (p,q) )
consider p, q being object such that
A1: ( p in L & q in L ) and
A2: p <> q by ZFMISC_1:def 10;
reconsider p = p, q = q as Point of V by A1;
take p ; :: thesis: ex q being Point of V st
( p <> q & L = Line (p,q) )
take q ; :: thesis: ( p <> q & L = Line (p,q) )
thus p <> q by A2; :: thesis: L = Line (p,q)
ex x1, x2 being Element of V st L = Line (x1,x2) by Def15;
hence L = Line (p,q) by A2, Th75, A1; :: thesis: verum