let it1, it2 be set ; :: thesis: ( ( for x being object holds

( x in it1 iff x is strict covariant Functor of A,B ) ) & ( for x being object holds

( x in it2 iff x is strict covariant Functor of A,B ) ) implies it1 = it2 )

assume that

A23: for x being object holds

( x in it1 iff x is strict covariant Functor of A,B ) and

A24: for x being object holds

( x in it2 iff x is strict covariant Functor of A,B ) ; :: thesis: it1 = it2

( x in it1 iff x is strict covariant Functor of A,B ) ) & ( for x being object holds

( x in it2 iff x is strict covariant Functor of A,B ) ) implies it1 = it2 )

assume that

A23: for x being object holds

( x in it1 iff x is strict covariant Functor of A,B ) and

A24: for x being object holds

( x in it2 iff x is strict covariant Functor of A,B ) ; :: thesis: it1 = it2

now :: thesis: for x being object holds

( x in it1 iff x in it2 )

hence
it1 = it2
by TARSKI:2; :: thesis: verum( x in it1 iff x in it2 )

let x be object ; :: thesis: ( x in it1 iff x in it2 )

( x in it1 iff x is strict covariant Functor of A,B ) by A23;

hence ( x in it1 iff x in it2 ) by A24; :: thesis: verum

end;( x in it1 iff x is strict covariant Functor of A,B ) by A23;

hence ( x in it1 iff x in it2 ) by A24; :: thesis: verum