let AFP be AffinPlane; for a, b, x, y being Element of AFP st not LIN a,b,x & a,b // x,y & a,x // b,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 & a,x // b,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:
a,x // b,y
; ( not LIN x,y,a & not LIN b,a,y & not LIN y,x,b )
x <> y
hence
( not LIN x,y,a & not LIN b,a,y & not LIN y,x,b )
by A1, A2, Lm4; verum