:: deftheorem defines L-Field MEASUR12:def 11 :
L-Field = COM (Borel_Sets,B-Meas);