defpred S1[ object , object ] means ex a, b, c being Element of BK_model st
( $1 = [a,b] & $2 = c & BK_to_REAL2 b in LSeg ((BK_to_REAL2 a),(BK_to_REAL2 c)) );
consider R being Relation of [:BK_model,BK_model:],BK_model such that
A1:
for x being Element of [:BK_model,BK_model:]
for y being Element of BK_model holds
( [x,y] in R iff S1[x,y] )
from RELSET_1:sch 2();
for a, b, c being Element of BK_model holds
( [[a,b],c] in R iff BK_to_REAL2 b in LSeg ((BK_to_REAL2 a),(BK_to_REAL2 c)) )
proof
let a,
b,
c be
Element of
BK_model ;
( [[a,b],c] in R iff BK_to_REAL2 b in LSeg ((BK_to_REAL2 a),(BK_to_REAL2 c)) )
hereby ( BK_to_REAL2 b in LSeg ((BK_to_REAL2 a),(BK_to_REAL2 c)) implies [[a,b],c] in R )
assume A2:
[[a,b],c] in R
;
BK_to_REAL2 b in LSeg ((BK_to_REAL2 a),(BK_to_REAL2 c))reconsider x =
[a,b] as
Element of
[:BK_model,BK_model:] ;
consider a9,
b9,
c9 being
Element of
BK_model such that A3:
x = [a9,b9]
and A4:
c = c9
and A5:
BK_to_REAL2 b9 in LSeg (
(BK_to_REAL2 a9),
(BK_to_REAL2 c9))
by A2, A1;
(
a = a9 &
b = b9 )
by A3, XTUPLE_0:1;
hence
BK_to_REAL2 b in LSeg (
(BK_to_REAL2 a),
(BK_to_REAL2 c))
by A4, A5;
verum
end;
assume
BK_to_REAL2 b in LSeg (
(BK_to_REAL2 a),
(BK_to_REAL2 c))
;
[[a,b],c] in R
hence
[[a,b],c] in R
by A1;
verum
end;
hence
ex b1 being Relation of [:BK_model,BK_model:],BK_model st
for a, b, c being Element of BK_model holds
( [[a,b],c] in b1 iff BK_to_REAL2 b in LSeg ((BK_to_REAL2 a),(BK_to_REAL2 c)) )
; verum