let S be OrderSortedSign; :: thesis: for X being set holds
( X is OperName of S iff ex op1 being OperSymbol of S st X = Name op1 )
let X be set ; :: thesis: ( X is OperName of S iff ex op1 being OperSymbol of S st X = Name op1 )

hereby :: thesis: ( ex op1 being OperSymbol of S st X = Name op1 implies X is OperName of S )

assume X is OperName of S ; :: thesis: ex x1 being OperSymbol of S st X = Name x1
then consider x being object such that
A1: x in the carrier' of S and
A2: X = Class ( the Overloading of S,x) by EQREL_1:def 3;
reconsider x1 = x as OperSymbol of S by A1;
take x1 = x1; :: thesis: X = Name x1
thus X = Name x1 by A2; :: thesis: verum

end;

given op1 being OperSymbol of S such that A3: X = Name op1 ; :: thesis: X is OperName of S
thus X is OperName of S by A3; :: thesis: verum