let B1, B2 be Relation of [:BK_model,BK_model:],[:BK_model,BK_model:]; :: 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 & (homography N) . a = c & (homography N) . 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 & (homography N) . a = c & (homography N) . 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 & (homography N) . a = c & (homography N) . 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 & (homography N) . a = c & (homography N) . 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 [:BK_model,BK_model:] & b in [:BK_model,BK_model:] ) 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 A7, ZFMISC_1:def 2;
ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st
( h = homography N & (homography N) . a1 = b1 & (homography N) . 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 [:BK_model,BK_model:] & b in [:BK_model,BK_model:] ) 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 A14bis, ZFMISC_1:def 2;
ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st
( h = homography N & (homography N) . a1 = b1 & (homography N) . 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;