A2: Int (right_cell (f,1)) c= RightComp f by GOBOARD9:def 2;
1 + 1 <= len f by GOBOARD7:34, XXREAL_0:2;
hence not RightComp f is empty by A2, GOBOARD9:16, XBOOLE_1:3; :: thesis: verum