let AFP be AffinPlane; :: thesis: for a, b being Element of AFP
for K being Subset of AFP st a,b // K & not a in K holds
for y being Element of AFP ex x being Element of AFP st
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) )
let a, b be Element of AFP; :: thesis: for K being Subset of AFP st a,b // K & not a in K holds
for y being Element of AFP ex x being Element of AFP st
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) )
let K be Subset of AFP; :: thesis: ( a,b // K & not a in K implies for y being Element of AFP ex x being Element of AFP st
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) )
assume that
A1: a,b // K and
A2: not a in K ; :: thesis: for y being Element of AFP ex x being Element of AFP st
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) )
let y be Element of AFP; :: thesis: ex x being Element of AFP st
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) )
A3: b,a // K by A1, AFF_1:34;
A4: not b in K by A1, A2, AFF_1:35;
then consider x being Element of AFP such that
A5: ( ( y in K & y = x ) or ( not y in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,b // p9,y & p,a // p9,x & y,x // K ) ) ) by A3, Lm19;
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) by A3, A4, A5, Lm18;
hence ex x being Element of AFP st
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ; :: thesis: verum