let AS be AffinSpace; 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); 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
; 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
; 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
; ( 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; ( 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
( b <> c & c <> a )proof
assume
not
a <> b
;
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;
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
c <> aproof
assume
not
b <> c
;
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;
verum
end;
thus
c <> a
verumproof
assume
not
c <> a
;
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;
verum
end;