defpred S₁[ 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₁[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 ) )

proof

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 ) )

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 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;

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 ) ; :: thesis: [[a,b],[c,d]] in R
hence [[a,b],[c,d]] in R by A1; :: thesis: verum

end;

hence ex b₁ 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₁ 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