deffunc H₁( non empty IntervalSet of U, non empty IntervalSet of U) -> IntervalSet of U = $1 _\/_ $2;
deffunc H₂( non empty IntervalSet of U, non empty IntervalSet of U) -> IntervalSet of U = $1 _/\_ $2;
set B = IntervalSets U;
defpred S₁[ Element of IntervalSets U, Element of IntervalSets U, Element of IntervalSets U] means ex a', b' being non empty IntervalSet of U st
( a' = $1 & b' = $2 & $3 = a' _\/_ b' );
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 x' = x, y' = y as non empty IntervalSet of U by DefAG;
reconsider z = x' _\/_ y' as Element of IntervalSets U by DefAG;
take z ; :: thesis: S₁[x,y,z]
thus S₁[x,y,z] ; :: thesis: verum

end;

consider B1 being BinOp of IntervalSets U such that
A6: 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 a', b' being non empty IntervalSet of U st
( a' = $1 & b' = $2 & $3 = a' _/\_ b' );
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 x' = x, y' = y as non empty IntervalSet of U by DefAG;
reconsider z = x' _/\_ y' as Element of IntervalSets U by DefAG;
take z ; :: thesis: S₂[x,y,z]
thus S₂[x,y,z] ; :: thesis: verum

end;

consider B2 being BinOp of IntervalSets U such that
A7: for x, y being Element of IntervalSets U holds S₂[x,y,B2 . x,y] from BINOP_1:sch 3(A1);
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 a', b' being non empty IntervalSet of U st a' = a & b' = b holds
( the L_join of IT . a,b = a' _\/_ b' & the L_meet of IT . a,b = a' _/\_ b' ) ) )
thus the carrier of IT = IntervalSets U ; :: thesis: for a, b being Element of the carrier of IT
for a', b' being non empty IntervalSet of U st a' = a & b' = b holds
( the L_join of IT . a,b = a' _\/_ b' & the L_meet of IT . a,b = a' _/\_ b' )
let a, b be Element of the carrier of IT; :: thesis: for a', b' being non empty IntervalSet of U st a' = a & b' = b holds
( the L_join of IT . a,b = a' _\/_ b' & the L_meet of IT . a,b = a' _/\_ b' )
let a', b' be non empty IntervalSet of U; :: thesis: ( a' = a & b' = b implies ( the L_join of IT . a,b = a' _\/_ b' & the L_meet of IT . a,b = a' _/\_ b' ) )
assume F0: ( a' = a & b' = b ) ; :: thesis: ( the L_join of IT . a,b = a' _\/_ b' & the L_meet of IT . a,b = a' _/\_ b' )
reconsider x = a, y = b as Element of IntervalSets U ;
consider a', b' being non empty IntervalSet of U such that
F1: ( a' = x & b' = y & B1 . x,y = a' _\/_ b' ) by A6;
consider a1, b1 being non empty IntervalSet of U such that
F2: ( a1 = x & b1 = y & B2 . x,y = a1 _/\_ b1 ) by A7;
thus ( the L_join of IT . a,b = a' _\/_ b' & the L_meet of IT . a,b = a' _/\_ b' ) by F1, F2, F0; :: thesis: verum