consider x being object 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, Def10;
hence not OSClass (E,s1) is empty ; :: thesis: verum