let AS be AffinSpace; :: thesis: for a, b being Element of AS

for A being Subset of AS st A is being_line & a in A & b in A & a <> b holds

A = Line (a,b)

let a, b be Element of AS; :: thesis: for A being Subset of AS st A is being_line & a in A & b in A & a <> b holds

A = Line (a,b)

let A be Subset of AS; :: thesis: ( A is being_line & a in A & b in A & a <> b implies A = Line (a,b) )

assume that

A1: A is being_line and

A2: a in A and

A3: b in A and

A4: a <> b ; :: thesis: A = Line (a,b)

A5: ex p, q being Element of AS st

( p <> q & A = Line (p,q) ) by A1;

then A6: A c= Line (a,b) by A2, A3, Th16;

Line (a,b) c= A by A2, A3, A4, A5, Th15;

hence A = Line (a,b) by A6, XBOOLE_0:def 10; :: thesis: verum

for A being Subset of AS st A is being_line & a in A & b in A & a <> b holds

A = Line (a,b)

let a, b be Element of AS; :: thesis: for A being Subset of AS st A is being_line & a in A & b in A & a <> b holds

A = Line (a,b)

let A be Subset of AS; :: thesis: ( A is being_line & a in A & b in A & a <> b implies A = Line (a,b) )

assume that

A1: A is being_line and

A2: a in A and

A3: b in A and

A4: a <> b ; :: thesis: A = Line (a,b)

A5: ex p, q being Element of AS st

( p <> q & A = Line (p,q) ) by A1;

then A6: A c= Line (a,b) by A2, A3, Th16;

Line (a,b) c= A by A2, A3, A4, A5, Th15;

hence A = Line (a,b) by A6, XBOOLE_0:def 10; :: thesis: verum