let AFP be AffinPlane; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( not LIN x,y,a & not LIN b,a,y & not LIN y,x,b )
x <> y

proof

assume x = y ; :: thesis: contradiction
then x,a // x,b by A3, AFF_1:4;
then LIN x,a,b by AFF_1:def 1;
hence contradiction by A1, AFF_1:6; :: thesis: verum

end;

hence ( not LIN x,y,a & not LIN b,a,y & not LIN y,x,b ) by A1, A2, Lm4; :: thesis: verum