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

suppose P in absolute ; :: thesis: ex b₁ being non zero Element of (TOP-REAL 3) st
( Dir b₁ = P & b₁ . 3 = 1 )

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;

suppose P in BK_model ; :: thesis: ex b₁ being non zero Element of (TOP-REAL 3) st
( Dir b₁ = P & b₁ . 3 = 1 )

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;

end;