set B = IntervalSets U;
defpred S1[ Element of IntervalSets U, Element of IntervalSets U, Element of IntervalSets U] means ex a9, b9 being non empty IntervalSet of U st
( a9 = $1 & b9 = $2 & $3 = a9 _\/_ b9 );
A1:
for x, y being Element of IntervalSets U ex z being Element of IntervalSets U st S1[x,y,z]
consider B1 being BinOp of (IntervalSets U) such that
A2:
for x, y being Element of IntervalSets U holds S1[x,y,B1 . (x,y)]
from BINOP_1:sch 3(A1);
defpred S2[ Element of IntervalSets U, Element of IntervalSets U, Element of IntervalSets U] means ex a9, b9 being non empty IntervalSet of U st
( a9 = $1 & b9 = $2 & $3 = a9 _/\_ b9 );
A3:
for x, y being Element of IntervalSets U ex z being Element of IntervalSets U st S2[x,y,z]
consider B2 being BinOp of (IntervalSets U) such that
A4:
for x, y being Element of IntervalSets U holds S2[x,y,B2 . (x,y)]
from BINOP_1:sch 3(A3);
take IT = LattStr(# (IntervalSets U),B1,B2 #); ( the carrier of IT = IntervalSets U & ( for a, b being Element of the carrier of IT
for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
( the L_join of IT . (a,b) = a9 _\/_ b9 & the L_meet of IT . (a,b) = a9 _/\_ b9 ) ) )
thus
the carrier of IT = IntervalSets U
; for a, b being Element of the carrier of IT
for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
( the L_join of IT . (a,b) = a9 _\/_ b9 & the L_meet of IT . (a,b) = a9 _/\_ b9 )
let a, b be Element of the carrier of IT; for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
( the L_join of IT . (a,b) = a9 _\/_ b9 & the L_meet of IT . (a,b) = a9 _/\_ b9 )
let a9, b9 be non empty IntervalSet of U; ( a9 = a & b9 = b implies ( the L_join of IT . (a,b) = a9 _\/_ b9 & the L_meet of IT . (a,b) = a9 _/\_ b9 ) )
assume A5:
( a9 = a & b9 = b )
; ( the L_join of IT . (a,b) = a9 _\/_ b9 & the L_meet of IT . (a,b) = a9 _/\_ b9 )
reconsider x = a, y = b as Element of IntervalSets U ;
consider a9, b9 being non empty IntervalSet of U such that
A6:
( a9 = x & b9 = y & B1 . (x,y) = a9 _\/_ b9 )
by A2;
consider a1, b1 being non empty IntervalSet of U such that
A7:
( a1 = x & b1 = y & B2 . (x,y) = a1 _/\_ b1 )
by A4;
thus
( the L_join of IT . (a,b) = a9 _\/_ b9 & the L_meet of IT . (a,b) = a9 _/\_ b9 )
by A6, A7, A5; verum