let AS be AffinSpace; :: thesis: for A being LINE of (IncProjSp_of AS) ex a, b, c being POINT of (IncProjSp_of AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
let A be LINE of (IncProjSp_of AS); :: thesis: ex a, b, c being POINT of (IncProjSp_of AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
consider X being Subset of AS such that
A1: ( ( A = [X,1] & X is being_line ) or ( A = [(PDir X),2] & X is being_plane ) ) by Th23;
A2: now :: thesis: ( A = [(PDir X),2] & X is being_plane implies ex a, b, c being POINT of (IncProjSp_of AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a ) )
assume that
A3: A = [(PDir X),2] and
A4: X is being_plane ; :: thesis: ex a, b, c being POINT of (IncProjSp_of AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
consider x, y, z being Element of AS such that
A5: x in X and
A6: y in X and
A7: z in X and
A8: not LIN x,y,z by A4, AFF_4:34;
A9: y <> z by A8, AFF_1:7;
then A10: Line (y,z) is being_line by AFF_1:def 3;
then A11: Line (y,z) '||' X by A4, A6, A7, A9, AFF_4:19, AFF_4:42;
A12: z <> x by A8, AFF_1:7;
then A13: Line (x,z) is being_line by AFF_1:def 3;
then A14: Line (x,z) '||' X by A4, A5, A7, A12, AFF_4:19, AFF_4:42;
A15: x <> y by A8, AFF_1:7;
then A16: Line (x,y) is being_line by AFF_1:def 3;
then reconsider a = LDir (Line (x,y)), b = LDir (Line (y,z)), c = LDir (Line (x,z)) as POINT of (IncProjSp_of AS) by A10, A13, Th20;
take a = a; :: thesis: ex b, c being POINT of (IncProjSp_of AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
take b = b; :: thesis: ex c being POINT of (IncProjSp_of AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
take c = c; :: thesis: ( a on A & b on A & c on A & a <> b & b <> c & c <> a )
Line (x,y) '||' X by A4, A5, A6, A15, A16, AFF_4:19, AFF_4:42;
hence ( a on A & b on A & c on A ) by A3, A4, A16, A10, A13, A11, A14, Th29; :: thesis: ( a <> b & b <> c & c <> a )
A17: x in Line (x,y) by AFF_1:15;
A18: z in Line (y,z) by AFF_1:15;
A19: y in Line (x,y) by AFF_1:15;
A20: y in Line (y,z) by AFF_1:15;
thus a <> b :: thesis: ( b <> c & c <> a )
proof
assume not a <> b ; :: thesis: contradiction
then Line (x,y) // Line (y,z) by A16, A10, Th11;
then z in Line (x,y) by A19, A20, A18, AFF_1:45;
hence contradiction by A8, A16, A17, A19, AFF_1:21; :: thesis: verum
end;
A21: z in Line (x,z) by AFF_1:15;
A22: x in Line (x,z) by AFF_1:15;
thus b <> c :: thesis: c <> a
proof
assume not b <> c ; :: thesis: contradiction
then Line (y,z) // Line (x,z) by A10, A13, Th11;
then x in Line (y,z) by A18, A22, A21, AFF_1:45;
hence contradiction by A8, A10, A20, A18, AFF_1:21; :: thesis: verum
end;
thus c <> a :: thesis: verum
proof
assume not c <> a ; :: thesis: contradiction
then Line (x,y) // Line (x,z) by A16, A13, Th11;
then z in Line (x,y) by A17, A22, A21, AFF_1:45;
hence contradiction by A8, A16, A17, A19, AFF_1:21; :: thesis: verum
end;
end;
now :: thesis: ( A = [X,1] & X is being_line implies ex a, b being Element of the Points of (IncProjSp_of AS) ex c being POINT of (IncProjSp_of AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a ) )
assume that
A23: A = [X,1] and
A24: X is being_line ; :: thesis: ex a, b being Element of the Points of (IncProjSp_of AS) ex c being POINT of (IncProjSp_of AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
reconsider c = LDir X as POINT of (IncProjSp_of AS) by A24, Th20;
consider x, y being Element of AS such that
A25: x in X and
A26: y in X and
A27: x <> y by A24, AFF_1:19;
reconsider a = x, b = y as Element of the Points of (IncProjSp_of AS) by Th20;
take a = a; :: thesis: ex b being Element of the Points of (IncProjSp_of AS) ex c being POINT of (IncProjSp_of AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
take b = b; :: thesis: ex c being POINT of (IncProjSp_of AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
take c = c; :: thesis: ( a on A & b on A & c on A & a <> b & b <> c & c <> a )
X // X by A24, AFF_1:41;
then X '||' X by A24, AFF_4:40;
hence ( a on A & b on A & c on A ) by A23, A24, A25, A26, Th26, Th28; :: thesis: ( a <> b & b <> c & c <> a )
thus a <> b by A27; :: thesis: ( b <> c & c <> a )
thus ( b <> c & c <> a ) :: thesis: verum
proof
assume A28: ( not b <> c or not c <> a ) ; :: thesis: contradiction
c in Dir_of_Lines AS by A24, Th14;
then the carrier of AS /\ (Dir_of_Lines AS) <> {} by A28, XBOOLE_0:def 4;
then the carrier of AS meets Dir_of_Lines AS by XBOOLE_0:def 7;
hence contradiction by Th16; :: thesis: verum
end;
end;
hence ex a, b, c being POINT of (IncProjSp_of AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a ) by A1, A2; :: thesis: verum