defpred S1[ 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 & () . a = c & () . b = d ) );
consider R being Relation of , such that
A1: for x, y being Element of holds
( [x,y] in R iff S1[x,y] ) from 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 & () . a = c & () . 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 & () . a = c & () . b = d ) )

hereby :: thesis: ( ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st
( h = homography N & () . a = c & () . 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 & () . a = c & () . b = d )

reconsider x = [a,b], y = [c,d] as Element of ;
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 & () . a9 = c9 & () . b9 = d9 ) ) by A2, A1;
( a = a9 & b = b9 & c = c9 & d = d9 ) by ;
hence ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st
( h = homography N & () . a = c & () . 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 & () . a = c & () . b = d ) ; :: thesis: [[a,b],[c,d]] in R
hence [[a,b],[c,d]] in R by A1; :: thesis: verum
end;
hence ex b1 being Relation of , st
for a, b, c, d being Element of BK_model holds
( [[a,b],[c,d]] in b1 iff ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st
( h = homography N & () . a = c & () . b = d ) ) ; :: thesis: verum