let X be Element of OperNames S; :: thesis: not X is empty
ex x being object st
( x in the carrier' of S & X = Class ( the Overloading of S,x) ) by EQREL_1:def 3;
hence not X is empty by EQREL_1:20; :: thesis: verum