let IPP be IncProjSp; for a, b, c, d being POINT of IPP
for A, B being LINE of IPP st ex o being POINT of IPP st
( o on A & o on B ) & a on A & b on A & c on A & d on A & a,b,c,d are_mutually_distinct holds
ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_distinct )
let a, b, c, d be POINT of IPP; for A, B being LINE of IPP st ex o being POINT of IPP st
( o on A & o on B ) & a on A & b on A & c on A & d on A & a,b,c,d are_mutually_distinct holds
ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_distinct )
let A, B be LINE of IPP; ( ex o being POINT of IPP st
( o on A & o on B ) & a on A & b on A & c on A & d on A & a,b,c,d are_mutually_distinct implies ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_distinct ) )
assume that
A1:
ex o being POINT of IPP st
( o on A & o on B )
and
A2:
a on A
and
A3:
b on A
and
A4:
c on A
and
A5:
d on A
and
A6:
a,b,c,d are_mutually_distinct
; ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_distinct )
consider o being POINT of IPP such that
A7:
o on A
and
A8:
o on B
by A1;
now ( A <> B implies ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_distinct ) )assume
A <> B
;
ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_distinct )then consider x,
y being
POINT of
IPP such that A9:
x on A
and A10:
not
x on B
and A11:
y on B
and A12:
not
y on A
by Th3;
consider C being
LINE of
IPP such that A13:
x on C
and A14:
y on C
by INCPROJ:def 5;
consider w being
POINT of
IPP such that A15:
w on C
and A16:
w <> x
and A17:
w <> y
by Th8;
A18:
now for u1, u2, v1, v2 being POINT of IPP
for D1, D2 being LINE of IPP st u1 on A & u2 on A & v1 on B & w on D1 & u1 on D1 & v1 on D1 & v2 on B & w on D2 & u2 on D2 & v2 on D2 & u1 <> u2 holds
not v1 = v2A19:
not
w on B
by A10, A11, A13, A14, A15, A17, INCPROJ:def 4;
let u1,
u2,
v1,
v2 be
POINT of
IPP;
for D1, D2 being LINE of IPP st u1 on A & u2 on A & v1 on B & w on D1 & u1 on D1 & v1 on D1 & v2 on B & w on D2 & u2 on D2 & v2 on D2 & u1 <> u2 holds
not v1 = v2let D1,
D2 be
LINE of
IPP;
( u1 on A & u2 on A & v1 on B & w on D1 & u1 on D1 & v1 on D1 & v2 on B & w on D2 & u2 on D2 & v2 on D2 & u1 <> u2 implies not v1 = v2 )assume that A20:
(
u1 on A &
u2 on A )
and A21:
v1 on B
and A22:
w on D1
and A23:
u1 on D1
and A24:
v1 on D1
and
v2 on B
and A25:
w on D2
and A26:
u2 on D2
and A27:
v2 on D2
;
( u1 <> u2 implies not v1 = v2 )A28:
D1 <> A
by A9, A12, A13, A14, A15, A16, A22, INCPROJ:def 4;
assume A29:
u1 <> u2
;
not v1 = v2assume
v1 = v2
;
contradictionthen
D1 = D2
by A21, A22, A24, A25, A27, A19, INCPROJ:def 4;
hence
contradiction
by A20, A23, A26, A29, A28, INCPROJ:def 4;
verum end; A30:
now for u being POINT of IPP st u on A holds
ex v being POINT of IPP ex D being LINE of IPP st
( v on B & w on D & u on D & v on D )let u be
POINT of
IPP;
( u on A implies ex v being POINT of IPP ex D being LINE of IPP st
( v on B & w on D & u on D & v on D ) )assume A31:
u on A
;
ex v being POINT of IPP ex D being LINE of IPP st
( v on B & w on D & u on D & v on D )A32:
now ( u <> o & x <> u implies ex v being POINT of IPP ex D being LINE of IPP st
( v on B & w on D & u on D & v on D ) )assume that
u <> o
and A33:
x <> u
;
ex v being POINT of IPP ex D being LINE of IPP st
( v on B & w on D & u on D & v on D )consider D being
LINE of
IPP such that A34:
(
w on D &
u on D )
by INCPROJ:def 5;
not
x on D
proof
assume
x on D
;
contradiction
then
u on C
by A13, A15, A16, A34, INCPROJ:def 4;
hence
contradiction
by A9, A12, A13, A14, A31, A33, INCPROJ:def 4;
verum
end; then consider v being
POINT of
IPP such that A35:
(
v on B &
v on D )
by A7, A8, A9, A10, A11, A12, A13, A14, A15, A31, A34, INCPROJ:def 8;
take v =
v;
ex D being LINE of IPP st
( v on B & w on D & u on D & v on D )take D =
D;
( v on B & w on D & u on D & v on D )thus
(
v on B &
w on D &
u on D &
v on D )
by A34, A35;
verum end; now ( u = o implies ex v being POINT of IPP ex D being LINE of IPP st
( v on B & w on D & u on D & v on D ) )consider D being
LINE of
IPP such that A36:
(
w on D &
u on D )
by INCPROJ:def 5;
assume A37:
u = o
;
ex v being POINT of IPP ex D being LINE of IPP st
( v on B & w on D & u on D & v on D )take v =
o;
ex D being LINE of IPP st
( v on B & w on D & u on D & v on D )take D =
D;
( v on B & w on D & u on D & v on D )thus
(
v on B &
w on D &
u on D &
v on D )
by A8, A37, A36;
verum end; hence
ex
v being
POINT of
IPP ex
D being
LINE of
IPP st
(
v on B &
w on D &
u on D &
v on D )
by A11, A13, A14, A15, A32;
verum end; then consider p being
POINT of
IPP,
D1 being
Element of the
Lines of
IPP such that A38:
p on B
and A39:
(
w on D1 &
a on D1 &
p on D1 )
by A2;
consider r being
POINT of
IPP,
D3 being
Element of the
Lines of
IPP such that A40:
r on B
and A41:
(
w on D3 &
c on D3 &
r on D3 )
by A4, A30;
consider q being
POINT of
IPP,
D2 being
Element of the
Lines of
IPP such that A42:
q on B
and A43:
(
w on D2 &
b on D2 &
q on D2 )
by A3, A30;
consider s being
POINT of
IPP,
D4 being
Element of the
Lines of
IPP such that A44:
s on B
and A45:
(
w on D4 &
d on D4 &
s on D4 )
by A5, A30;
d <> a
by A6, ZFMISC_1:def 6;
then A46:
s <> p
by A2, A5, A18, A38, A39, A45;
a <> c
by A6, ZFMISC_1:def 6;
then A47:
p <> r
by A2, A4, A18, A38, A39, A41;
d <> b
by A6, ZFMISC_1:def 6;
then A48:
s <> q
by A3, A5, A18, A42, A43, A45;
c <> d
by A6, ZFMISC_1:def 6;
then A49:
r <> s
by A4, A5, A18, A40, A41, A45;
b <> c
by A6, ZFMISC_1:def 6;
then A50:
q <> r
by A3, A4, A18, A42, A43, A41;
a <> b
by A6, ZFMISC_1:def 6;
then
p <> q
by A2, A3, A18, A38, A39, A43;
then
p,
q,
r,
s are_mutually_distinct
by A50, A49, A46, A48, A47, ZFMISC_1:def 6;
hence
ex
p,
q,
r,
s being
POINT of
IPP st
(
p on B &
q on B &
r on B &
s on B &
p,
q,
r,
s are_mutually_distinct )
by A38, A42, A40, A44;
verum end;
hence
ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_distinct )
by A2, A3, A4, A5, A6; verum