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