defpred S₁[ 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 S₁[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 ; :: thesis: ( [[a,b],c] in R iff BK_to_REAL2 b in LSeg ((BK_to_REAL2 a),(BK_to_REAL2 c)) )

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

end;

assume BK_to_REAL2 b in LSeg ((BK_to_REAL2 a),(BK_to_REAL2 c)) ; :: thesis: [[a,b],c] in R
hence [[a,b],c] in R by A1; :: thesis: verum

end;

hence ex b₁ being Relation of [:BK_model,BK_model:],BK_model st
for a, b, c being Element of BK_model holds
( [[a,b],c] in b₁ iff BK_to_REAL2 b in LSeg ((BK_to_REAL2 a),(BK_to_REAL2 c)) ) ; :: thesis: verum