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:16;
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:16;
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:16;
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:26;
A16: z in Line y,z by AFF_1:26;
A17: y in Line x,y by AFF_1:26;
A18: y in Line y,z by AFF_1:26;
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:59;
hence contradiction by A6, A14, A15, A17, AFF_1:33; :: thesis: verum

end;

A19: z in Line x,z by AFF_1:26;
A20: x in Line x,z by AFF_1:26;
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:59;
hence contradiction by A6, A8, A18, A16, AFF_1:33; :: 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:59;
hence contradiction by A6, A14, A15, A17, AFF_1:33; :: thesis: verum

end;