per cases
( P in absolute or P in BK_model )
by A0, XBOOLE_0:def 3;

end;

suppose
P in absolute
; :: thesis: ex b_{1} being non zero Element of (TOP-REAL 3) st

( Dir b_{1} = P & b_{1} . 3 = 1 )

( Dir b

then reconsider P1 = P as Element of absolute ;

consider u being non zero Element of (TOP-REAL 3) such that

A1: ( P1 = Dir u & u . 3 = 1 ) and

absolute_to_REAL2 P1 = |[(u . 1),(u . 2)]| by BKMODEL1:def 8;

take u ; :: thesis: ( Dir u = P & u . 3 = 1 )

thus ( Dir u = P & u . 3 = 1 ) by A1; :: thesis: verum

end;consider u being non zero Element of (TOP-REAL 3) such that

A1: ( P1 = Dir u & u . 3 = 1 ) and

absolute_to_REAL2 P1 = |[(u . 1),(u . 2)]| by BKMODEL1:def 8;

take u ; :: thesis: ( Dir u = P & u . 3 = 1 )

thus ( Dir u = P & u . 3 = 1 ) by A1; :: thesis: verum

suppose
P in BK_model
; :: thesis: ex b_{1} being non zero Element of (TOP-REAL 3) st

( Dir b_{1} = P & b_{1} . 3 = 1 )

( Dir b

then reconsider P1 = P as Element of BK_model ;

consider u being non zero Element of (TOP-REAL 3) such that

A2: ( Dir u = P1 & u . 3 = 1 ) and

BK_to_REAL2 P1 = |[(u . 1),(u . 2)]| by BKMODEL2:def 2;

take u ; :: thesis: ( Dir u = P & u . 3 = 1 )

thus ( Dir u = P & u . 3 = 1 ) by A2; :: thesis: verum

end;consider u being non zero Element of (TOP-REAL 3) such that

A2: ( Dir u = P1 & u . 3 = 1 ) and

BK_to_REAL2 P1 = |[(u . 1),(u . 2)]| by BKMODEL2:def 2;

take u ; :: thesis: ( Dir u = P & u . 3 = 1 )

thus ( Dir u = P & u . 3 = 1 ) by A2; :: thesis: verum