let AFP be AffinPlane; for a, b, x, y being Element of AFP st not LIN a,b,x & a,b // x,y & x <> y holds
( not LIN x,y,a & not LIN b,a,y & not LIN y,x,b )
let a, b, x, y be Element of AFP; ( not LIN a,b,x & a,b // x,y & x <> y implies ( not LIN x,y,a & not LIN b,a,y & not LIN y,x,b ) )
assume that
A1:
not LIN a,b,x
and
A2:
a,b // x,y
and
A3:
x <> y
; ( not LIN x,y,a & not LIN b,a,y & not LIN y,x,b )
thus
not LIN x,y,a
( not LIN b,a,y & not LIN y,x,b )proof
A4:
LIN x,
y,
x
by AFF_1:7;
assume A5:
LIN x,
y,
a
;
contradiction
x,
y // a,
b
by A2, AFF_1:4;
then
LIN x,
y,
b
by A3, A5, AFF_1:9;
hence
contradiction
by A1, A3, A5, A4, AFF_1:8;
verum
end;
thus
not LIN b,a,y
not LIN y,x,bproof
assume A6:
LIN b,
a,
y
;
contradiction
(
b,
a // y,
x &
b <> a )
by A1, A2, AFF_1:4, AFF_1:7;
then
LIN b,
a,
x
by A6, AFF_1:9;
hence
contradiction
by A1, AFF_1:6;
verum
end;
thus
not LIN y,x,b
verumproof
A7:
LIN y,
x,
x
by AFF_1:7;
assume A8:
LIN y,
x,
b
;
contradiction
y,
x // b,
a
by A2, AFF_1:4;
then
LIN y,
x,
a
by A3, A8, AFF_1:9;
hence
contradiction
by A1, A3, A8, A7, AFF_1:8;
verum
end;