:: deftheorem Def12 defines InterLatt INTERVA1:def 12 :
for U being non empty set
for b₂ being non empty strict LattStr holds
( b₂ = InterLatt U iff ( the carrier of b₂ = IntervalSets U & ( for a, b being Element of the carrier of b₂
for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
( the L_join of b₂ . (a,b) = a9 _\/_ b9 & the L_meet of b₂ . (a,b) = a9 _/\_ b9 ) ) ) );