set O = { f where f is morphism of C : ( f is identity & f in Mor C ) } ;
for x being object st x in { f where f is morphism of C : ( f is identity & f in Mor C ) } holds
x in Mor C

proof

let x be object ; :: thesis: ( x in { f where f is morphism of C : ( f is identity & f in Mor C ) } implies x in Mor C )
assume x in { f where f is morphism of C : ( f is identity & f in Mor C ) } ; :: thesis: x in Mor C
then consider f being morphism of C such that
A1: ( x = f & f is identity & f in Mor C ) ;
thus x in Mor C by A1; :: thesis: verum

end;

hence { f where f is morphism of C : ( f is identity & f in Mor C ) } is Subset of (Mor C) by TARSKI:def 3; :: thesis: verum