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 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 :: 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 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;
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 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;
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;
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