assume
not BK_model misses absolute
; contradiction
then consider x being object such that
A1:
x in BK_model /\ absolute
by XBOOLE_0:def 1;
A2:
( x in BK_model & x in absolute )
by A1, XBOOLE_0:def 4;
x in { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (1,1,(- 1),0,0,0,u) = 0 }
by A2, PASCAL:def 2;
then consider P being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A3:
x = P
and
A4:
for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (1,1,(- 1),0,0,0,u) = 0
;
consider u being Element of (TOP-REAL 3) such that
A5:
not u is zero
and
A6:
P = Dir u
by ANPROJ_1:26;
consider Q being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A7:
x = Q
and
A8:
for u being Element of (TOP-REAL 3) st not u is zero & Q = Dir u holds
qfconic (1,1,(- 1),0,0,0,u) is negative
by A2;
( qfconic (1,1,(- 1),0,0,0,u) = 0 & qfconic (1,1,(- 1),0,0,0,u) is negative )
by A3, A4, A5, A6, A7, A8;
hence
contradiction
; verum