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 ) )
proof
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 )

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 ) )
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 ;
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;
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 ) )
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 ;
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;
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 ) )
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 ; :: thesis: verum
end;
hence ex A being Subset of AS st
( A is being_line & a in A & b in A & c in A ) by A3, A7; :: thesis: verum
end;
( ex A being Subset of AS st
( A is being_line & a in A & b in A & c in A ) implies LIN a,b,c )
proof
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 ;
A22: LIN p,q,c by ;
LIN p,q,a by ;
hence LIN a,b,c by A19, A21, A22, Th7; :: thesis: verum
end;
hence ( 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 ) ) by A1; :: thesis: verum