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

end;

thus not LIN b,a,y :: thesis: not LIN y,x,b

proof

assume A6: LIN b,a,y ; :: thesis: 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; :: thesis: verum

end;

thus not LIN y,x,b :: thesis: verum

proof

A7: LIN y,x,x by AFF_1:7;
assume A8: LIN y,x,b ; :: thesis: 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; :: thesis: verum

end;