defpred S_{1}[ object , object ] means ex a, b, c, d being Element of BK_model st

( $1 = [a,b] & $2 = [c,d] & ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st

( h = homography N & (homography N) . a = c & (homography N) . b = d ) );

consider R being Relation of [:BK_model,BK_model:],[:BK_model,BK_model:] such that

A1: for x, y being Element of [:BK_model,BK_model:] holds

( [x,y] in R iff S_{1}[x,y] )
from RELSET_1:sch 2();

for a, b, c, d being Element of BK_model holds

( [[a,b],[c,d]] in R iff ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st

( h = homography N & (homography N) . a = c & (homography N) . b = d ) )_{1} being Relation of [:BK_model,BK_model:],[:BK_model,BK_model:] st

for a, b, c, d being Element of BK_model holds

( [[a,b],[c,d]] in b_{1} iff ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st

( h = homography N & (homography N) . a = c & (homography N) . b = d ) ) ; :: thesis: verum

( $1 = [a,b] & $2 = [c,d] & ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st

( h = homography N & (homography N) . a = c & (homography N) . b = d ) );

consider R being Relation of [:BK_model,BK_model:],[:BK_model,BK_model:] such that

A1: for x, y being Element of [:BK_model,BK_model:] holds

( [x,y] in R iff S

for a, b, c, d being Element of BK_model holds

( [[a,b],[c,d]] in R iff ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st

( h = homography N & (homography N) . a = c & (homography N) . b = d ) )

proof

hence
ex b
let a, b, c, d be Element of BK_model ; :: thesis: ( [[a,b],[c,d]] in R iff ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st

( h = homography N & (homography N) . a = c & (homography N) . b = d ) )

( h = homography N & (homography N) . a = c & (homography N) . b = d ) ; :: thesis: [[a,b],[c,d]] in R

hence [[a,b],[c,d]] in R by A1; :: thesis: verum

end;( h = homography N & (homography N) . a = c & (homography N) . b = d ) )

hereby :: thesis: ( ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st

( h = homography N & (homography N) . a = c & (homography N) . b = d ) implies [[a,b],[c,d]] in R )

assume
ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st ( h = homography N & (homography N) . a = c & (homography N) . b = d ) implies [[a,b],[c,d]] in R )

assume A2:
[[a,b],[c,d]] in R
; :: thesis: ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st

( h = homography N & (homography N) . a = c & (homography N) . b = d )

reconsider x = [a,b], y = [c,d] as Element of [:BK_model,BK_model:] ;

consider a9, b9, c9, d9 being Element of BK_model such that

A3: ( x = [a9,b9] & y = [c9,d9] & ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st

( h = homography N & (homography N) . a9 = c9 & (homography N) . b9 = d9 ) ) by A2, A1;

( a = a9 & b = b9 & c = c9 & d = d9 ) by A3, XTUPLE_0:1;

hence ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st

( h = homography N & (homography N) . a = c & (homography N) . b = d ) by A3; :: thesis: verum

end;( h = homography N & (homography N) . a = c & (homography N) . b = d )

reconsider x = [a,b], y = [c,d] as Element of [:BK_model,BK_model:] ;

consider a9, b9, c9, d9 being Element of BK_model such that

A3: ( x = [a9,b9] & y = [c9,d9] & ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st

( h = homography N & (homography N) . a9 = c9 & (homography N) . b9 = d9 ) ) by A2, A1;

( a = a9 & b = b9 & c = c9 & d = d9 ) by A3, XTUPLE_0:1;

hence ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st

( h = homography N & (homography N) . a = c & (homography N) . b = d ) by A3; :: thesis: verum

( h = homography N & (homography N) . a = c & (homography N) . b = d ) ; :: thesis: [[a,b],[c,d]] in R

hence [[a,b],[c,d]] in R by A1; :: thesis: verum

for a, b, c, d being Element of BK_model holds

( [[a,b],[c,d]] in b

( h = homography N & (homography N) . a = c & (homography N) . b = d ) ) ; :: thesis: verum