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 x being Element of AFP ex y 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 x being Element of AFP ex y 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 x being Element of AFP ex y 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 x being Element of AFP ex y 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: not b in K by A1, A2, AFF_1:35;
A4: K is being_line by A1, AFF_1:26;
let x be Element of AFP; :: thesis: ex y 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 ) ) )
consider p, q being Element of AFP such that
A5: p in K and
q in K and
p <> q by A1, AFF_1:19, AFF_1:26;
A6: p <> b by A1, A2, A5, AFF_1:35;
now :: thesis: ( not x in K implies ex y 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 ) ) ) )
set B9 = Line (p,b);
set A = Line (p,a);
assume A7: not x in K ; :: thesis: ex y 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 ) ) )
A8: a in Line (p,a) by AFF_1:15;
Line (p,a) is being_line by A2, A5, AFF_1:def 3;
then consider C being Subset of AFP such that
A9: x in C and
A10: Line (p,a) // C by AFF_1:49;
A11: C is being_line by A10, AFF_1:36;
A12: p in Line (p,a) by AFF_1:15;
then not Line (p,a) // K by A2, A5, A8, AFF_1:45;
then not C // K by A10, AFF_1:44;
then consider p9 being Element of AFP such that
A13: p9 in C and
A14: p9 in K by A4, A11, AFF_1:58;
Line (p,b) is being_line by A6, AFF_1:def 3;
then consider D being Subset of AFP such that
A15: p9 in D and
A16: Line (p,b) // D by AFF_1:49;
A17: b in Line (p,b) by AFF_1:15;
K is being_line by A1, AFF_1:26;
then consider M being Subset of AFP such that
A18: x in M and
A19: K // M by AFF_1:49;
A20: M is being_line by A19, AFF_1:36;
A21: p in Line (p,b) by AFF_1:15;
then A22: not Line (p,b) // K by A5, A3, A17, AFF_1:45;
A23: not D // M
proof
assume D // M ; :: thesis: contradiction
then Line (p,b) // M by A16, AFF_1:44;
hence contradiction by A22, A19, AFF_1:44; :: thesis: verum
end;
D is being_line by A16, AFF_1:36;
then consider y being Element of AFP such that
A24: y in D and
A25: y in M by A20, A23, AFF_1:58;
A26: p,b // p9,y by A21, A17, A15, A16, A24, AFF_1:39;
A27: x,y // K by A18, A19, A25, AFF_1:40;
p,a // p9,x by A12, A8, A9, A10, A13, AFF_1:39;
hence ex y 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 ) ) ) by A5, A7, A14, A27, A26; :: thesis: verum
end;
hence ex y 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