let P be Element of absolute ; tangent P misses BK_model
assume
not tangent P misses BK_model
; contradiction
then consider x being object such that
A1:
x in tangent P
and
A2:
x in BK_model
by XBOOLE_0:3;
reconsider x = x as Element of real_projective_plane by A1;
reconsider L = tangent P as LINE of (IncProjSp_of real_projective_plane) by INCPROJ:4;
reconsider ip = P, iq = x as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:3;
( P in tangent P & x in tangent P )
by A1, Th21;
then
( ip on L & iq on L )
by INCPROJ:5;
then consider p1, p2 being POINT of (IncProjSp_of real_projective_plane), P1, P2 being Element of real_projective_plane such that
A3:
p1 = P1
and
A4:
p2 = P2
and
A5:
P1 <> P2
and
A6:
P1 in absolute
and
A7:
P2 in absolute
and
A8:
p1 on L
and
A9:
p2 on L
by A2, Th15;
( P1 in L & P2 in L )
by A3, A4, A8, A9, INCPROJ:5;
then
( P1 in (tangent P) /\ absolute & P2 in (tangent P) /\ absolute )
by A6, A7, XBOOLE_0:def 4;
then
( P1 in {P} & P2 in {P} )
by Th22;
then
( P1 = P & P2 = P )
by TARSKI:def 1;
hence
contradiction
by A5; verum