let SAS be AffinPlane; :: thesis: for o, a being Element of SAS ex p being Element of SAS st
for b, c being Element of SAS holds
( o,a // o,p & ex d being Element of SAS st
( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) )
let o, a be Element of SAS; :: thesis: ex p being Element of SAS st
for b, c being Element of SAS holds
( o,a // o,p & ex d being Element of SAS st
( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) )
ex p being Element of SAS st
( o <> p & o,a // o,p )

proof

consider x, y being Element of SAS such that
A1: x <> y by DIRAF:47;

now

assume a = o ; :: thesis: ex p being Element of SAS st
( o <> p & o,a // o,p )
then A2: ( o,a // o,x & o,a // o,y ) by AFF_1:12;
( o <> x or o <> y ) by A1;
hence ex p being Element of SAS st
( o <> p & o,a // o,p ) by A2; :: thesis: verum

end;

hence ex p being Element of SAS st
( o <> p & o,a // o,p ) by AFF_1:11; :: thesis: verum

end;

then consider p being Element of SAS such that
A3: o <> p and
A4: o,a // o,p ;
take p ; :: thesis: for b, c being Element of SAS holds
( o,a // o,p & ex d being Element of SAS st
( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) )
thus for b, c being Element of SAS holds
( o,a // o,p & ex d being Element of SAS st
( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ) :: thesis: verum

proof

let b, c be Element of SAS; :: thesis: ( o,a // o,p & ex d being Element of SAS st
( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) )
ex d being Element of SAS st
( o,p // o,b implies ( o,c // o,d & p,c // b,d ) )

proof

now

assume o,p // o,b ; :: thesis: ex d being Element of SAS st
( o,p // o,b implies ( o,c // o,d & p,c // b,d ) )
then p,o // o,b by AFF_1:13;
then consider d being Element of SAS such that
A5: ( c,o // o,d & c,p // b,d ) by A3, DIRAF:47;
( o,c // o,d & p,c // b,d ) by A5, AFF_1:13;
hence ex d being Element of SAS st
( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ; :: thesis: verum

end;

hence ex d being Element of SAS st
( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ; :: thesis: verum

end;

hence ( o,a // o,p & ex d being Element of SAS st
( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ) by A4; :: thesis: verum

end;