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;
A2: ( a <> o implies ex p being Element of SAS st
( o <> p & o,a // o,p ) ) by AFF_1:11;

now

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

end;

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

end;

then consider p being Element of SAS such that
A6: ( o <> p & 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
A7: ( c,o // o,d & c,p // b,d ) by A6, DIRAF:47;
( o,c // o,d & p,c // b,d ) by A7, 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 A6; :: thesis: verum

end;