let C, D be Category; :: thesis: NatTrans (C,D) c= [:[:(bool [: the carrier' of C, the carrier' of D:]),(bool [: the carrier' of C, the carrier' of D:]):],(bool [: the carrier of C, the carrier' of D:]):]
set CD = [: the carrier' of C, the carrier' of D:];
set CDp = [: the carrier of C, the carrier' of D:];

now :: thesis: for x being set st x in NatTrans (C,D) holds
x in [:[:(bool [: the carrier' of C, the carrier' of D:]),(bool [: the carrier' of C, the carrier' of D:]):],(bool [: the carrier of C, the carrier' of D:]):]

let x be set ; :: thesis: ( x in NatTrans (C,D) implies x in [:[:(bool [: the carrier' of C, the carrier' of D:]),(bool [: the carrier' of C, the carrier' of D:]):],(bool [: the carrier of C, the carrier' of D:]):] )
assume x in NatTrans (C,D) ; :: thesis: x in [:[:(bool [: the carrier' of C, the carrier' of D:]),(bool [: the carrier' of C, the carrier' of D:]):],(bool [: the carrier of C, the carrier' of D:]):]
then consider F1, F2 being Functor of C,D such that
A1: ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) by NATTRA_1:def 16;
consider t being natural_transformation of F1,F2 such that
A2: ( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) by A1;
[F1,F2] in [:(bool [: the carrier' of C, the carrier' of D:]),(bool [: the carrier' of C, the carrier' of D:]):] by ZFMISC_1:def 2;
hence x in [:[:(bool [: the carrier' of C, the carrier' of D:]),(bool [: the carrier' of C, the carrier' of D:]):],(bool [: the carrier of C, the carrier' of D:]):] by A2, ZFMISC_1:def 2; :: thesis: verum

end;

hence NatTrans (C,D) c= [:[:(bool [: the carrier' of C, the carrier' of D:]),(bool [: the carrier' of C, the carrier' of D:]):],(bool [: the carrier of C, the carrier' of D:]):] ; :: thesis: verum