let AFP be AffinPlane; :: thesis: for a, b, x, y being Element of
for K being Subset of st a,b // K & not a in K & ( ( x in K & x = y ) or ( not x in K & ex p, p' being Element of st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) holds
( b,a // K & not b in K & ( ( y in K & y = x ) or ( not y in K & ex p, p' being Element of st
( p in K & p' in K & p,b // p',y & p,a // p',x & y,x // K ) ) ) )
let a, b, x, y be Element of ; :: thesis: for K being Subset of st a,b // K & not a in K & ( ( x in K & x = y ) or ( not x in K & ex p, p' being Element of st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) holds
( b,a // K & not b in K & ( ( y in K & y = x ) or ( not y in K & ex p, p' being Element of st
( p in K & p' in K & p,b // p',y & p,a // p',x & y,x // K ) ) ) )
let K be Subset of ; :: thesis: ( a,b // K & not a in K & ( ( x in K & x = y ) or ( not x in K & ex p, p' being Element of st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) implies ( b,a // K & not b in K & ( ( y in K & y = x ) or ( not y in K & ex p, p' being Element of st
( p in K & p' in K & p,b // p',y & p,a // p',x & y,x // K ) ) ) ) )
assume that
A1: a,b // K and
A2: not a in K and
A3: ( ( x in K & x = y ) or ( not x in K & ex p, p' being Element of st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) ; :: thesis: ( b,a // K & not b in K & ( ( y in K & y = x ) or ( not y in K & ex p, p' being Element of st
( p in K & p' in K & p,b // p',y & p,a // p',x & y,x // K ) ) ) )

now

assume not x in K ; :: thesis: ( b,a // K & not b in K & ( ( y in K & y = x ) or ( not y in K & ex p, p' being Element of st
( p in K & p' in K & p,b // p',y & p,a // p',x & y,x // K ) ) ) )
then y,x // K by A3, AFF_1:48;
hence ( b,a // K & not b in K & ( ( y in K & y = x ) or ( not y in K & ex p, p' being Element of st
( p in K & p' in K & p,b // p',y & p,a // p',x & y,x // K ) ) ) ) by A1, A2, A3, AFF_1:48, AFF_1:49; :: thesis: verum

end;

hence ( b,a // K & not b in K & ( ( y in K & y = x ) or ( not y in K & ex p, p' being Element of st
( p in K & p' in K & p,b // p',y & p,a // p',x & y,x // K ) ) ) ) by A1, A2, A3, AFF_1:48, AFF_1:49; :: thesis: verum