consider X being set such that
A4: for x being set holds
( x in X iff ( x in the carrier of F₁() & P₁[x] ) ) from XBOOLE_0:sch 1();
consider a0 being object of F₁() such that
A5: P₁[a0] by A1;
reconsider X = X as non empty set by A4, A5;
A6: X c= the carrier of F₁()

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
thus ( not x in X or x in the carrier of F₁() ) by A4; :: thesis:

end;

deffunc H₁( set , set ) -> set = the Arrows of F₁() . $1,$2;
deffunc H₂( set , set , set , set , set ) -> set = (the Comp of F₁() . $1,$2,$3) . $5,$4;

A7: now

let a, b, c be Element of X; :: thesis:
let f, g be set ; :: thesis:
assume that
A8: ( f in H₁(a,b) & P₂[a,b,f] ) and
A9: ( g in H₁(b,c) & P₂[b,c,g] ) ; :: thesis:
reconsider a' = a, b' = b, c' = c as object of F₁() by A4;
A10: H₁(a,b) = <^a',b'^> ;
reconsider f' = f as Morphism of a',b' by A8;
A11: H₁(b,c) = <^b',c'^> ;
reconsider g' = g as Morphism of b',c' by A9;
A12: ( H₂(a,b,c,f,g) = g' * f' & H₁(a,c) = <^a',c'^> & <^a',c'^> <> {} ) by A8, A9, A10, A11, ALTCAT_1:def 4, ALTCAT_1:def 10;
hence H₂(a,b,c,f,g) in H₁(a,c) ; :: thesis:
( P₁[a'] & P₁[b'] & P₁[c'] ) by A4;
hence P₂[a,c,H₂(a,b,c,f,g)] by A2, A8, A9, A12; :: thesis:

end;

A13: now

let a, b, c, d be Element of X; :: thesis:
let f, g, h be set ; :: thesis:
assume that
A14: ( f in H₁(a,b) & P₂[a,b,f] ) and
A15: ( g in H₁(b,c) & P₂[b,c,g] ) and
A16: ( h in H₁(c,d) & P₂[c,d,h] ) ; :: thesis:
reconsider a' = a, b' = b, c' = c, d' = d as object of F₁() by A4;
A17: H₁(a,b) = <^a',b'^> ;
reconsider f' = f as Morphism of a',b' by A14;
A18: H₁(b,c) = <^b',c'^> ;
reconsider g' = g as Morphism of b',c' by A15;
A19: H₁(c,d) = <^c',d'^> ;
reconsider h' = h as Morphism of c',d' by A16;
A20: ( <^a',c'^> <> {} & <^b',d'^> <> {} ) by A14, A15, A16, A17, A18, A19, ALTCAT_1:def 4;
thus H₂(a,c,d,H₂(a,b,c,f,g),h) = H₂(a',c',d',g' * f',h) by A14, A15, ALTCAT_1:def 10
.= h' * (g' * f') by A16, A20, ALTCAT_1:def 10
.= (h' * g') * f' by A14, A15, A16, ALTCAT_1:25
.= H₂(a,b,d,f,h' * g') by A14, A20, ALTCAT_1:def 10
.= H₂(a,b,d,f,H₂(b,c,d,g,h)) by A15, A16, ALTCAT_1:def 10 ; :: thesis:

end;

A21: now

let a be Element of X; :: thesis:
reconsider b = a as object of F₁() by A4;
reconsider f = idm b as set ;
take f = f; :: thesis:
( H₁(a,a) = <^b,b^> & P₁[b] ) by A4;
hence ( f in H₁(a,a) & P₂[a,a,f] ) by A3; :: thesis:
let c be Element of X; :: thesis:
let g be set ; :: thesis:
assume A22: ( g in H₁(a,c) & P₂[a,c,g] ) ; :: thesis:
reconsider d = c as object of F₁() by A4;
reconsider g' = g as Morphism of b,d by A22;
thus H₂(a,a,c,f,g) = g' * (idm b) by A22, ALTCAT_1:def 10
.= g by A22, ALTCAT_1:def 19 ; :: thesis:

end;

A23: now

let a be Element of X; :: thesis:
reconsider b = a as object of F₁() by A4;
reconsider f = idm b as set ;
take f = f; :: thesis:
( H₁(a,a) = <^b,b^> & P₁[b] ) by A4;
hence ( f in H₁(a,a) & P₂[a,a,f] ) by A3; :: thesis:
let c be Element of X; :: thesis:
let g be set ; :: thesis:
assume A24: ( g in H₁(c,a) & P₂[c,a,g] ) ; :: thesis:
reconsider d = c as object of F₁() by A4;
reconsider g' = g as Morphism of d,b by A24;
thus H₂(c,a,a,g,f) = (idm b) * g' by A24, ALTCAT_1:def 10
.= g by A24, ALTCAT_1:24 ; :: thesis:

end;

consider C being strict category such that
A25: the carrier of C = X and
A26: for a, b being object of C
for f being set holds
( f in <^a,b^> iff ( f in H₁(a,b) & P₂[a,b,f] ) ) and
A27: for a, b, c being object of C st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = H₂(a,b,c,f,g) from YELLOW18:sch 6(A7, A13, A21, A23);
C is SubCatStr of F₁()

proof

thus the carrier of C c= the carrier of F₁() by A6, A25; :: according to ALTCAT_2:def 11 :: thesis:
thus [:the carrier of C,the carrier of C:] c= [:the carrier of F₁(),the carrier of F₁():] by A6, A25, ZFMISC_1:119; :: according to ALTCAT_2:def 2 :: thesis:

hereby :: thesis:

let i be set ; :: thesis:
assume i in [:the carrier of C,the carrier of C:] ; :: thesis:
then consider a, b being set such that
A28: ( a in the carrier of C & b in the carrier of C & [a,b] = i ) by ZFMISC_1:def 2;
reconsider a = a, b = b as object of C by A28;
A29: the Arrows of C . i = <^a,b^> by A28;
A30: the Arrows of F₁() . i = the Arrows of F₁() . a,b by A28;
thus the Arrows of C . i c= the Arrows of F₁() . i :: thesis:

proof

let f be set ; :: according to TARSKI:def 3 :: thesis:
thus ( not f in the Arrows of C . i or f in the Arrows of F₁() . i ) by A26, A29, A30; :: thesis:

end;

thus [:the carrier of C,the carrier of C,the carrier of C:] c= [:the carrier of F₁(),the carrier of F₁(),the carrier of F₁():] by A6, A25, MCART_1:77; :: according to ALTCAT_2:def 2 :: thesis:
let i be set ; :: thesis:
assume i in [:the carrier of C,the carrier of C,the carrier of C:] ; :: thesis:
then consider a, b, c being set such that
A31: ( a in the carrier of C & b in the carrier of C & c in the carrier of C & [a,b,c] = i ) by MCART_1:72;
reconsider a = a, b = b, c = c as object of C by A31;
reconsider a' = a, b' = b, c' = c as object of F₁() by A4, A25;
let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in the Comp of C . i ; :: thesis:
then A32: x in the Comp of C . a,b,c by A31, MULTOP_1:def 1;
then consider gf, h being set such that
A33: x = [gf,h] and
A34: gf in [:(the Arrows of C . b,c),(the Arrows of C . a,b):] and
A35: h in the Arrows of C . a,c by RELSET_1:6;
consider g, f being set such that
A36: ( g in the Arrows of C . b,c & f in the Arrows of C . a,b & [g,f] = gf ) by A34, ZFMISC_1:def 2;
reconsider f = f as Morphism of a,b by A36;
reconsider g = g as Morphism of b,c by A36;
reconsider h = h as Morphism of a,c by A35;
A37: the Comp of F₁() . a',b',c' = the Comp of F₁() . i by A31, MULTOP_1:def 1;
A38: ( g in the Arrows of F₁() . b',c' & f in the Arrows of F₁() . a',b' ) by A26, A36;
A39: h = (the Comp of C . a,b,c) . g,f by A32, A33, A36, FUNCT_1:8
.= g * f by A36, ALTCAT_1:def 10
.= (the Comp of F₁() . a',b',c') . g,f by A27, A36 ;
h in the Arrows of F₁() . a',c' by A26, A35;
then dom (the Comp of F₁() . a',b',c') = [:(the Arrows of F₁() . b',c'),(the Arrows of F₁() . a',b'):] by FUNCT_2:def 1;
then ( gf in dom (the Comp of F₁() . a',b',c') & h = (the Comp of F₁() . a',b',c') . gf ) by A36, A38, A39, ZFMISC_1:def 2;
hence x in the Comp of F₁() . i by A33, A37, FUNCT_1:def 4; :: thesis:

end;

then reconsider C = C as non empty SubCatStr of F₁() ;
for o being object of C
for o' being object of F₁() st o = o' holds
idm o' in <^o,o^>

proof

let a be object of C; :: thesis:
let b be object of F₁(); :: thesis:
assume A40: a = b ; :: thesis:
then ( idm b in <^b,b^> & P₁[b] ) by A4, A25;
then ( idm b in the Arrows of F₁() . b,b & P₂[b,b, idm b] ) by A3;
hence idm b in <^a,a^> by A26, A40; :: thesis:

end;

then reconsider C = C as non empty strict subcategory of F₁() by ALTCAT_2:def 14;
take C ; :: thesis:
thus for a being object of F₁() holds
( a is object of C iff P₁[a] ) by A4, A25; :: thesis:
let a, b be object of F₁(); :: thesis:
let a', b' be object of C; :: thesis:
assume A41: ( a' = a & b' = b & <^a,b^> <> {} ) ; :: thesis:
let f be Morphism of a,b; :: thesis:
thus ( f in <^a',b'^> iff P₂[a,b,f] ) by A26, A41; :: thesis: