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

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

end;( [a,b] in B1 iff [a,b] in B2 )

proof

hence
B1 = B2
by RELAT_1:def 2; :: thesis: verum
let a, b be object ; :: thesis: ( [a,b] in B1 iff [a,b] in B2 )

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;hereby :: thesis: ( [a,b] in B2 implies [a,b] in B1 )

assume A14:
[a,b] in B2
; :: thesis: [a,b] in B1assume 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;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

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