let R1, R2 be Relation of [:BK_model,BK_model:],BK_model; :: thesis: ( ( 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)) ) ; :: thesis: R1 = R2

thus R1 = R2 :: thesis: verum

( [[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)) ) ; :: thesis: R1 = R2

thus R1 = R2 :: thesis: verum

proof

for a, b being object holds

( [a,b] in R1 iff [a,b] in R2 )

end;( [a,b] in R1 iff [a,b] in R2 )

proof

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

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; :: thesis: verum

end;hereby :: thesis: ( [a,b] in R2 implies [a,b] in R1 )

assume A15:
[a,b] in R2
; :: thesis: [a,b] in R1assume A8:
[a,b] in R1
; :: thesis: [a,b] in R2

then 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; :: thesis: verum

end;then 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; :: thesis: verum

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; :: thesis: verum