defpred S_{1}[ set , set , set ] means verum;

A2: for a, b, c being Object of F_{1}() st P_{1}[a] & P_{1}[b] & P_{1}[c] & <^a,b^> <> {} & <^b,c^> <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c st S_{1}[a,b,f] & S_{1}[b,c,g] holds

S_{1}[a,c,g * f]
;

A3: for a being Object of F_{1}() st P_{1}[a] holds

S_{1}[a,a, idm a]
;

A4: ex a being Object of F_{1}() st P_{1}[a]
by A1;

consider B being non empty strict subcategory of F_{1}() such that

A5: for a being Object of F_{1}() holds

( a is Object of B iff P_{1}[a] )
and

A6: for a, b being Object of F_{1}()

for a9, b9 being Object of B st a9 = a & b9 = b & <^a,b^> <> {} holds

for f being Morphism of a,b holds

( f in <^a9,b9^> iff S_{1}[a,b,f] )
from YELLOW18:sch 7(A4, A2, A3);

hence ex B being non empty strict full subcategory of F_{1}() st

for a being Object of F_{1}() holds

( a is Object of B iff P_{1}[a] )
by A5; :: thesis: verum

A2: for a, b, c being Object of F

for f being Morphism of a,b

for g being Morphism of b,c st S

S

A3: for a being Object of F

S

A4: ex a being Object of F

consider B being non empty strict subcategory of F

A5: for a being Object of F

( a is Object of B iff P

A6: for a, b being Object of F

for a9, b9 being Object of B st a9 = a & b9 = b & <^a,b^> <> {} holds

for f being Morphism of a,b holds

( f in <^a9,b9^> iff S

now :: thesis: for a1, a2 being Object of F_{1}()

for b1, b2 being Object of B st b1 = a1 & b2 = a2 holds

<^b1,b2^> = <^a1,a2^>

then
B is full
by Th26;for b1, b2 being Object of B st b1 = a1 & b2 = a2 holds

<^b1,b2^> = <^a1,a2^>

let a1, a2 be Object of F_{1}(); :: thesis: for b1, b2 being Object of B st b1 = a1 & b2 = a2 holds

<^b1,b2^> = <^a1,a2^>

let b1, b2 be Object of B; :: thesis: ( b1 = a1 & b2 = a2 implies <^b1,b2^> = <^a1,a2^> )

assume A7: ( b1 = a1 & b2 = a2 ) ; :: thesis: <^b1,b2^> = <^a1,a2^>

A8: <^a1,a2^> c= <^b1,b2^> by A6, A7;

<^b1,b2^> c= <^a1,a2^> by A7, ALTCAT_2:31;

hence <^b1,b2^> = <^a1,a2^> by A8; :: thesis: verum

end;<^b1,b2^> = <^a1,a2^>

let b1, b2 be Object of B; :: thesis: ( b1 = a1 & b2 = a2 implies <^b1,b2^> = <^a1,a2^> )

assume A7: ( b1 = a1 & b2 = a2 ) ; :: thesis: <^b1,b2^> = <^a1,a2^>

A8: <^a1,a2^> c= <^b1,b2^> by A6, A7;

<^b1,b2^> c= <^a1,a2^> by A7, ALTCAT_2:31;

hence <^b1,b2^> = <^a1,a2^> by A8; :: thesis: verum

hence ex B being non empty strict full subcategory of F

for a being Object of F

( a is Object of B iff P