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

set A = Line a,b;
A4: a in Line a,b by Th26;
A5: b in Line a,b by Th26;
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 by Def3;
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;

A7: now

set A = Line a,c;
A8: c in Line a,c by Th26;
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 by Def3;
LIN a,c,b by A2, Th15;
then A10: b in Line a,c by Def2;
a in Line a,c by Th26;
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

consider x being Element of AS such that
A11: a <> x by Th10;
set A = Line a,x;
A12: a in Line a,x by Th26;
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, Def3;
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;

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, Def3;
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, Th17; :: 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