:: deftheorem Def4 defines (#) COUSIN:def 5 :
for Iac, Icb being non empty closed_interval Subset of REAL
for Dac being Division of Iac
for Dcb being Division of Icb st upper_bound Iac <= lower_bound Icb holds
( ( Dcb . 1 <> upper_bound Iac implies Dac (#) Dcb = Dac ^ Dcb ) & ( not Dcb . 1 <> upper_bound Iac implies Dac (#) Dcb = Dac ^ (Dcb /^ 1) ) );