let R1, R2 be Relation of [:BK_model,BK_model:],BK_model; ( ( for a, b, c being Element of BK_model holds
( [[a,b],c] in R1 iff BK_to_REAL2 b in LSeg ((BK_to_REAL2 a),(BK_to_REAL2 c)) ) ) & ( for a, b, c being Element of BK_model holds
( [[a,b],c] in R2 iff BK_to_REAL2 b in LSeg ((BK_to_REAL2 a),(BK_to_REAL2 c)) ) ) implies R1 = R2 )
assume that
A6:
for a, b, c being Element of BK_model holds
( [[a,b],c] in R1 iff BK_to_REAL2 b in LSeg ((BK_to_REAL2 a),(BK_to_REAL2 c)) )
and
A7:
for a, b, c being Element of BK_model holds
( [[a,b],c] in R2 iff BK_to_REAL2 b in LSeg ((BK_to_REAL2 a),(BK_to_REAL2 c)) )
; R1 = R2
thus
R1 = R2
verumproof
for
a,
b being
object holds
(
[a,b] in R1 iff
[a,b] in R2 )
proof
let a,
b be
object ;
( [a,b] in R1 iff [a,b] in R2 )
hereby ( [a,b] in R2 implies [a,b] in R1 )
assume A8:
[a,b] in R1
;
[a,b] in R2then consider c,
d being
object such that A9:
[a,b] = [c,d]
and A10:
c in [:BK_model,BK_model:]
and A11:
d in BK_model
by RELSET_1:2;
consider e,
f being
object such that A12:
e in BK_model
and A13:
f in BK_model
and A14:
c = [e,f]
by A10, ZFMISC_1:def 2;
reconsider d =
d,
e =
e,
f =
f as
Element of
BK_model by A12, A13, A11;
BK_to_REAL2 f in LSeg (
(BK_to_REAL2 e),
(BK_to_REAL2 d))
by A6, A8, A9, A14;
hence
[a,b] in R2
by A9, A7, A14;
verum
end;
assume A15:
[a,b] in R2
;
[a,b] in R1
then consider c,
d being
object such that A16:
[a,b] = [c,d]
and A17:
c in [:BK_model,BK_model:]
and A18:
d in BK_model
by RELSET_1:2;
consider e,
f being
object such that A19:
e in BK_model
and A20:
f in BK_model
and A21:
c = [e,f]
by A17, ZFMISC_1:def 2;
reconsider d =
d,
e =
e,
f =
f as
Element of
BK_model by A19, A20, A18;
BK_to_REAL2 f in LSeg (
(BK_to_REAL2 e),
(BK_to_REAL2 d))
by A7, A15, A16, A21;
hence
[a,b] in R1
by A16, A6, A21;
verum
end;
hence
R1 = R2
by RELAT_1:def 2;
verum
end;