A1: Int (left_cell (f,1)) c= LeftComp f by GOBOARD9:def 1;
1 + 1 <= len f by GOBOARD7:34, XXREAL_0:2;
hence not LeftComp f is empty by A1, GOBOARD9:15, XBOOLE_1:3; :: thesis: verum