let R1, R2 be Relation of ,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 ((),()) ) ) & ( for a, b, c being Element of BK_model holds
( [[a,b],c] in R2 iff BK_to_REAL2 b in LSeg ((),()) ) ) 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 ((),()) ) and
A7: for a, b, c being Element of BK_model holds
( [[a,b],c] in R2 iff BK_to_REAL2 b in LSeg ((),()) ) ; :: 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 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 ;
reconsider d = d, e = e, f = f as Element of BK_model by ;
BK_to_REAL2 f in LSeg ((),()) 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 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 ;
reconsider d = d, e = e, f = f as Element of BK_model by ;
BK_to_REAL2 f in LSeg ((),()) 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;