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

proof

for a, b being object holds
( [a,b] in R1 iff [a,b] in R2 )

proof

let a, b be object ; :: thesis: ( [a,b] in R1 iff [a,b] in R2 )

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

assume 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;

assume A15: [a,b] in R2 ; :: thesis: [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; :: thesis: verum

end;

hence R1 = R2 by RELAT_1:def 2; :: thesis: verum

end;