let B1, B2 be Relation of [:BK_model,BK_model:],[:BK_model,BK_model:]; ( ( 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 ) )
; B1 = B2
thus
B1 = B2
verumproof
for
a,
b being
object holds
(
[a,b] in B1 iff
[a,b] in B2 )
proof
let a,
b be
object ;
( [a,b] in B1 iff [a,b] in B2 )
hereby ( [a,b] in B2 implies [a,b] in B1 )
assume A6:
[a,b] in B1
;
[a,b] in B2then 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;
verum
end;
assume A14:
[a,b] in B2
;
[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;
verum
end;
hence
B1 = B2
by RELAT_1:def 2;
verum
end;