set B = IntervalSets U;
defpred S₁[ 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 S₁[x,y,z]

proof

let x, y be Element of IntervalSets U; :: thesis: ex z being Element of IntervalSets U st S₁[x,y,z]
reconsider x9 = x, y9 = y as non empty IntervalSet of U by Def11;
reconsider z = x9 _\/_ y9 as Element of IntervalSets U by Def11;
take z ; :: thesis: S₁[x,y,z]
thus S₁[x,y,z] ; :: thesis: verum

end;

consider B1 being BinOp of (IntervalSets U) such that
A2: for x, y being Element of IntervalSets U holds S₁[x,y,B1 . (x,y)] from BINOP_1:sch 3(A1);
defpred S₂[ 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 S₂[x,y,z]

proof

let x, y be Element of IntervalSets U; :: thesis: ex z being Element of IntervalSets U st S₂[x,y,z]
reconsider x9 = x, y9 = y as non empty IntervalSet of U by Def11;
reconsider z = x9 _/\_ y9 as Element of IntervalSets U by Def11;
take z ; :: thesis: S₂[x,y,z]
thus S₂[x,y,z] ; :: thesis: verum

end;

consider B2 being BinOp of (IntervalSets U) such that
A4: for x, y being Element of IntervalSets U holds S₂[x,y,B2 . (x,y)] from BINOP_1:sch 3(A3);
take IT = LattStr(# (IntervalSets U),B1,B2 #); :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( 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; :: thesis: verum