let B1, B2 be Relation of ,; :: thesis: ( ( 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 ) ) ) & ( for a, b, c, d being Element of BK_model holds
( [[a,b],[c,d]] in B2 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 ) ) ) implies B1 = B2 )

assume that
A4: 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 ) ) and
A5: for a, b, c, d being Element of BK_model holds
( [[a,b],[c,d]] in B2 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: B1 = B2
thus B1 = B2 :: thesis: verum
proof
for a, b being object holds
( [a,b] in B1 iff [a,b] in B2 )
proof
let a, b be object ; :: thesis: ( [a,b] in B1 iff [a,b] in B2 )
hereby :: thesis: ( [a,b] in B2 implies [a,b] in B1 )
assume A6: [a,b] in B1 ; :: thesis: [a,b] in B2
then A7: ( a in & b in ) by ZFMISC_1:87;
then consider a1, a2 being object such that
A8: a1 in BK_model and
A9: a2 in BK_model and
A10: a = [a1,a2] by ZFMISC_1:def 2;
consider b1, b2 being object such that
A11: b1 in BK_model and
A12: b2 in BK_model and
A13: b = [b1,b2] by ;
ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st
( h = homography N & () . a1 = b1 & () . a2 = b2 ) by A4, A11, A12, A8, A9, A10, A6, A13;
hence [a,b] in B2 by A10, A13, A5, A8, A9, A11, A12; :: thesis: verum
end;
assume A14: [a,b] in B2 ; :: thesis: [a,b] in B1
then A14bis: ( a in & b in ) by ZFMISC_1:87;
then consider a1, a2 being object such that
A15: a1 in BK_model and
A16: a2 in BK_model and
A17: a = [a1,a2] by ZFMISC_1:def 2;
consider b1, b2 being object such that
A18: b1 in BK_model and
A19: b2 in BK_model and
A20: b = [b1,b2] by ;
ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st
( h = homography N & () . a1 = b1 & () . a2 = b2 ) by A5, A18, A19, A15, A16, A17, A14, A20;
hence [a,b] in B1 by A17, A20, A4, A15, A16, A18, A19; :: thesis: verum
end;
hence B1 = B2 by RELAT_1:def 2; :: thesis: verum
end;