set IT = { f where f is morphism of C : ex f1, f2 being morphism of C st

( a = f1 & b = f2 & f |> f1 & f2 |> f ) } ;

( a = f1 & b = f2 & f |> f1 & f2 |> f ) } is Subset of (Mor C) ; :: thesis: verum

( a = f1 & b = f2 & f |> f1 & f2 |> f ) } ;

now :: thesis: { f where f is morphism of C : ex f1, f2 being morphism of C st

( a = f1 & b = f2 & f |> f1 & f2 |> f ) } is Subset of (Mor C)

hence
{ f where f is morphism of C : ex f1, f2 being morphism of C st ( a = f1 & b = f2 & f |> f1 & f2 |> f ) } is Subset of (Mor C)

for x being object st x in { f where f is morphism of C : ex f1, f2 being morphism of C st

( a = f1 & b = f2 & f |> f1 & f2 |> f ) } holds

x in Mor C

( a = f1 & b = f2 & f |> f1 & f2 |> f ) } is Subset of (Mor C) by TARSKI:def 3; :: thesis: verum

end;( a = f1 & b = f2 & f |> f1 & f2 |> f ) } holds

x in Mor C

proof

hence
{ f where f is morphism of C : ex f1, f2 being morphism of C st
let x be object ; :: thesis: ( x in { f where f is morphism of C : ex f1, f2 being morphism of C st

( a = f1 & b = f2 & f |> f1 & f2 |> f ) } implies x in Mor C )

assume x in { f where f is morphism of C : ex f1, f2 being morphism of C st

( a = f1 & b = f2 & f |> f1 & f2 |> f ) } ; :: thesis: x in Mor C

then consider f being morphism of C such that

A1: ( x = f & ex f1, f2 being morphism of C st

( a = f1 & b = f2 & f |> f1 & f2 |> f ) ) ;

consider f1, f2 being morphism of C such that

A2: ( a = f1 & b = f2 & f |> f1 & f2 |> f ) by A1;

not C is empty by A2, CAT_6:1;

then not Mor C is empty ;

hence x in Mor C by A1; :: thesis: verum

end;( a = f1 & b = f2 & f |> f1 & f2 |> f ) } implies x in Mor C )

assume x in { f where f is morphism of C : ex f1, f2 being morphism of C st

( a = f1 & b = f2 & f |> f1 & f2 |> f ) } ; :: thesis: x in Mor C

then consider f being morphism of C such that

A1: ( x = f & ex f1, f2 being morphism of C st

( a = f1 & b = f2 & f |> f1 & f2 |> f ) ) ;

consider f1, f2 being morphism of C such that

A2: ( a = f1 & b = f2 & f |> f1 & f2 |> f ) by A1;

not C is empty by A2, CAT_6:1;

then not Mor C is empty ;

hence x in Mor C by A1; :: thesis: verum

( a = f1 & b = f2 & f |> f1 & f2 |> f ) } is Subset of (Mor C) by TARSKI:def 3; :: thesis: verum

( a = f1 & b = f2 & f |> f1 & f2 |> f ) } is Subset of (Mor C) ; :: thesis: verum