let AS be AffinSpace; :: thesis: for A being Element of the Lines of (ProjHorizon AS) ex a, b, c being Element of the Points of (ProjHorizon AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
let A be Element of the Lines of (ProjHorizon AS); :: thesis: ex a, b, c being Element of the Points of (ProjHorizon 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 = PDir X and
A2: X is being_plane by Th15;
consider x, y, z being Element of AS such that
A3: x in X and
A4: y in X and
A5: z in X and
A6: not LIN x,y,z by A2, AFF_4:34;
A7: y <> z by A6, AFF_1:7;
then A8: Line (y,z) is being_line by AFF_1:def 3;
then A9: Line (y,z) '||' X by A2, A4, A5, A7, AFF_4:19, AFF_4:42;
A10: z <> x by A6, AFF_1:7;
then A11: Line (x,z) is being_line by AFF_1:def 3;
then A12: Line (x,z) '||' X by A2, A3, A5, A10, AFF_4:19, AFF_4:42;
A13: x <> y by A6, AFF_1:7;
then A14: 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 Element of the Points of (ProjHorizon AS) by A8, A11, Th14;
take a ; :: thesis: ex b, c being Element of the Points of (ProjHorizon AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
take b ; :: thesis: ex c being Element of the Points of (ProjHorizon AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
take c ; :: thesis: ( a on A & b on A & c on A & a <> b & b <> c & c <> a )
Line (x,y) '||' X by A2, A3, A4, A13, A14, AFF_4:19, AFF_4:42;
hence ( a on A & b on A & c on A ) by A1, A2, A14, A8, A11, A9, A12, Th36; :: thesis: ( a <> b & b <> c & c <> a )
A15: x in Line (x,y) by AFF_1:15;
A16: z in Line (y,z) by AFF_1:15;
A17: y in Line (x,y) by AFF_1:15;
A18: 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 A14, A8, Th11;
then z in Line (x,y) by A17, A18, A16, AFF_1:45;
hence contradiction by A6, A14, A15, A17, AFF_1:21; :: thesis: verum

end;

A19: z in Line (x,z) by AFF_1:15;
A20: 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 A8, A11, Th11;
then x in Line (y,z) by A16, A20, A19, AFF_1:45;
hence contradiction by A6, A8, A18, A16, 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 A14, A11, Th11;
then z in Line (x,y) by A15, A20, A19, AFF_1:45;
hence contradiction by A6, A14, A15, A17, AFF_1:21; :: thesis: verum

end;