now :: thesis: for A being set st A in Borel_Sets holds
A in COM (Borel_Sets,B-Meas)

let A be set ; :: thesis: ( A in Borel_Sets implies A in COM (Borel_Sets,B-Meas) )
assume A1: A in Borel_Sets ; :: thesis: A in COM (Borel_Sets,B-Meas)
set B = A;
A = A \/ {} ;
hence A in COM (Borel_Sets,B-Meas) by A1, Th75, MEASURE3:def 3; :: thesis: verum

end;

hence Borel_Sets c= L-Field ; :: thesis: verum