per cases ( P in absolute or P in BK_model ) by A0, XBOOLE_0:def 3;
suppose P in absolute ; :: thesis: ex b1 being non zero Element of (TOP-REAL 3) st
( Dir b1 = P & b1 . 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 b1 being non zero Element of (TOP-REAL 3) st
( Dir b1 = P & b1 . 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;