let AS be AffinSpace; 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; 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; ( 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
; A = Line a,b
A5:
ex p, q being Element of AS st
( p <> q & A = Line p,q )
by A1, Def3;
then A6:
A c= Line a,b
by A2, A3, Th28;
Line a,b c= A
by A2, A3, A4, A5, Th27;
hence
A = Line a,b
by A6, XBOOLE_0:def 10; verum