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

( LIN a,b,c iff ex A being Subset of AS st

( A is being_line & a in A & b in A & c in A ) )

let a, b, c be Element of AS; :: thesis: ( LIN a,b,c iff ex A being Subset of AS st

( A is being_line & a in A & b in A & c in A ) )

A1: ( LIN a,b,c implies ex A being Subset of AS st

( A is being_line & a in A & b in A & c in A ) )

( A is being_line & a in A & b in A & c in A ) implies LIN a,b,c )

( A is being_line & a in A & b in A & c in A ) ) by A1; :: thesis: verum

( LIN a,b,c iff ex A being Subset of AS st

( A is being_line & a in A & b in A & c in A ) )

let a, b, c be Element of AS; :: thesis: ( LIN a,b,c iff ex A being Subset of AS st

( A is being_line & a in A & b in A & c in A ) )

A1: ( LIN a,b,c implies ex A being Subset of AS st

( A is being_line & a in A & b in A & c in A ) )

proof

( ex A being Subset of AS st
assume A2:
LIN a,b,c
; :: thesis: ex A being Subset of AS st

( A is being_line & a in A & b in A & c in A )

( A is being_line & a in A & b in A & c in A ) by A3, A7; :: thesis: verum

end;( A is being_line & a in A & b in A & c in A )

A3: now :: thesis: ( a <> b implies ex A being Subset of AS st

( A is being_line & a in A & b in A & c in A ) )

( A is being_line & a in A & b in A & c in A ) )

set A = Line (a,b);

A4: a in Line (a,b) by Th14;

A5: b in Line (a,b) by Th14;

assume a <> b ; :: thesis: ex A being Subset of AS st

( A is being_line & a in A & b in A & c in A )

then A6: Line (a,b) is being_line ;

c in Line (a,b) by A2, Def2;

hence ex A being Subset of AS st

( A is being_line & a in A & b in A & c in A ) by A6, A4, A5; :: thesis: verum

end;A4: a in Line (a,b) by Th14;

A5: b in Line (a,b) by Th14;

assume a <> b ; :: thesis: ex A being Subset of AS st

( A is being_line & a in A & b in A & c in A )

then A6: Line (a,b) is being_line ;

c in Line (a,b) by A2, Def2;

hence ex A being Subset of AS st

( A is being_line & a in A & b in A & c in A ) by A6, A4, A5; :: thesis: verum

A7: now :: thesis: ( a <> c implies ex A being Subset of AS st

( A is being_line & a in A & b in A & c in A ) )

( A is being_line & a in A & b in A & c in A ) )

set A = Line (a,c);

A8: c in Line (a,c) by Th14;

assume a <> c ; :: thesis: ex A being Subset of AS st

( A is being_line & a in A & b in A & c in A )

then A9: Line (a,c) is being_line ;

LIN a,c,b by A2, Th5;

then A10: b in Line (a,c) by Def2;

a in Line (a,c) by Th14;

hence ex A being Subset of AS st

( A is being_line & a in A & b in A & c in A ) by A9, A10, A8; :: thesis: verum

end;A8: c in Line (a,c) by Th14;

assume a <> c ; :: thesis: ex A being Subset of AS st

( A is being_line & a in A & b in A & c in A )

then A9: Line (a,c) is being_line ;

LIN a,c,b by A2, Th5;

then A10: b in Line (a,c) by Def2;

a in Line (a,c) by Th14;

hence ex A being Subset of AS st

( A is being_line & a in A & b in A & c in A ) by A9, A10, A8; :: thesis: verum

now :: thesis: ( a = b & a = c implies ex A being Subset of AS st

( A is being_line & a in A & b in A & c in A ) )

hence
ex A being Subset of AS st ( A is being_line & a in A & b in A & c in A ) )

consider x being Element of AS such that

A11: a <> x by SUBSET_1:50;

set A = Line (a,x);

A12: a in Line (a,x) by Th14;

assume that

A13: a = b and

A14: a = c ; :: thesis: ex A being Subset of AS st

( A is being_line & a in A & b in A & c in A )

Line (a,x) is being_line by A11;

hence ex A being Subset of AS st

( A is being_line & a in A & b in A & c in A ) by A13, A14, A12; :: thesis: verum

end;A11: a <> x by SUBSET_1:50;

set A = Line (a,x);

A12: a in Line (a,x) by Th14;

assume that

A13: a = b and

A14: a = c ; :: thesis: ex A being Subset of AS st

( A is being_line & a in A & b in A & c in A )

Line (a,x) is being_line by A11;

hence ex A being Subset of AS st

( A is being_line & a in A & b in A & c in A ) by A13, A14, A12; :: thesis: verum

( A is being_line & a in A & b in A & c in A ) by A3, A7; :: thesis: verum

( A is being_line & a in A & b in A & c in A ) implies LIN a,b,c )

proof

hence
( LIN a,b,c iff ex A being Subset of AS st
given A being Subset of AS such that A15:
A is being_line
and

A16: a in A and

A17: b in A and

A18: c in A ; :: thesis: LIN a,b,c

consider p, q being Element of AS such that

A19: p <> q and

A20: A = Line (p,q) by A15;

A21: LIN p,q,b by A17, A20, Def2;

A22: LIN p,q,c by A18, A20, Def2;

LIN p,q,a by A16, A20, Def2;

hence LIN a,b,c by A19, A21, A22, Th7; :: thesis: verum

end;A16: a in A and

A17: b in A and

A18: c in A ; :: thesis: LIN a,b,c

consider p, q being Element of AS such that

A19: p <> q and

A20: A = Line (p,q) by A15;

A21: LIN p,q,b by A17, A20, Def2;

A22: LIN p,q,c by A18, A20, Def2;

LIN p,q,a by A16, A20, Def2;

hence LIN a,b,c by A19, A21, A22, Th7; :: thesis: verum

( A is being_line & a in A & b in A & c in A ) ) by A1; :: thesis: verum