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

assume LIN x,y,a ; :: thesis: contradiction
then ( LIN x,y,a & x,y // a,b ) by A2, AFF_1:13;
then ( LIN x,y,a & LIN x,y,b & LIN x,y,x ) by A3, AFF_1:16, AFF_1:18;
hence contradiction by A1, A3, AFF_1:17; :: thesis: verum

end;

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

proof

assume LIN b,a,y ; :: thesis: contradiction
then ( LIN b,a,y & b,a // y,x & b <> a ) by A1, A2, AFF_1:13, AFF_1:16;
then LIN b,a,x by AFF_1:18;
hence contradiction by A1, AFF_1:15; :: thesis: verum

end;

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

proof

assume LIN y,x,b ; :: thesis: contradiction
then ( LIN y,x,b & y,x // b,a ) by A2, AFF_1:13;
then ( LIN y,x,b & LIN y,x,a & LIN y,x,x ) by A3, AFF_1:16, AFF_1:18;
hence contradiction by A1, A3, AFF_1:17; :: thesis: verum

end;