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
now :: thesis: for x being object holds
( 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;
hence it1 = it2 by TARSKI:2; :: thesis: verum