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