set X = { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 2 ) } ;
{ o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 2 ) } is infinite
by Def12;
then consider m1, m2 being object such that
A8:
( m1 in { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 2 ) } & m2 in { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 2 ) } & m1 <> m2 )
by ZFMISC_1:def 10;
consider o1 being OperSymbol of C such that
A9:
( m1 = o1 & the_result_sort_of o1 = s & len (the_arity_of o1) = 2 )
by A8;
consider o2 being OperSymbol of C such that
A10:
( m2 = o2 & the_result_sort_of o2 = s & len (the_arity_of o2) = 2 )
by A8;
reconsider m1 = m1, m2 = m2 as OperSymbol of s by A9, A10, ABCMIZ_1:def 32;
A11:
( m1 is binary & m2 is binary )
by A9, A10;
then A12:
( m1 <> non_op C & m2 <> non_op C )
by Th37;
( m1 <> * or m2 <> * )
by A8;
then
( m1 is constructor or m2 is constructor )
by A12;
hence
ex b1 being OperSymbol of s st
( b1 is binary & b1 is constructor )
by A11; verum