set B = IntervalSets U;

defpred S_{1}[ 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_{1}[x,y,z]

A2: for x, y being Element of IntervalSets U holds S_{1}[x,y,B1 . (x,y)]
from BINOP_1:sch 3(A1);

defpred S_{2}[ 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_{2}[x,y,z]

A4: for x, y being Element of IntervalSets U holds S_{2}[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

defpred S

( 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

proof

consider B1 being BinOp of (IntervalSets U) such that
let x, y be Element of IntervalSets U; :: thesis: ex z being Element of IntervalSets U st S_{1}[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_{1}[x,y,z]

thus S_{1}[x,y,z]
; :: thesis: verum

end;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

thus S

A2: for x, y being Element of IntervalSets U holds S

defpred S

( 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

proof

consider B2 being BinOp of (IntervalSets U) such that
let x, y be Element of IntervalSets U; :: thesis: ex z being Element of IntervalSets U st S_{2}[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_{2}[x,y,z]

thus S_{2}[x,y,z]
; :: thesis: verum

end;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

thus S

A4: for x, y being Element of IntervalSets U holds S

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