consider x being set such that
A1: x in the Sorts of A . s1 by XBOOLE_0:def 1;
Class (CompClass E,(CComp s1)),x in OSClass E,s1 by A1, Def12;
hence not OSClass E,s1 is empty ; :: thesis: verum