consider C being strict preorder category such that
A1: Ob C = 3 and
A2: for o1, o2 being Object of C st o1 in o2 holds
Hom (o1,o2) = {[o1,o2]} and
A3: RelOb C = RelIncl 3 and
A4: Mor C = 3 \/ { [o1,o2] where o1, o2 is Element of 3 : o1 in o2 } by CAT_7:37;
A5: C is 3 -ordered by A3, WELLORD1:38, CAT_7:def 14;
consider F being Functor of C,(OrdC 3), G being Functor of (OrdC 3),C such that
A6: ( F is covariant & G is covariant ) and
A7: ( G (*) F = id C & F (*) G = id (OrdC 3) ) by A5, CAT_7:38, CAT_6:def 28;
A8: ( 0 in 1 & 0 is Element of 3 & 1 is Element of 3 ) by CARD_1:49, CARD_1:51, TARSKI:def 1, ENUMSET1:def 1;
then A9: [0,1] in { [o1,o2] where o1, o2 is Element of 3 : o1 in o2 } ;
then A10: [0,1] in Mor C by A4, XBOOLE_0:def 3;
reconsider g1 = [0,1] as morphism of C by A9, A4, XBOOLE_0:def 3;
A11: not C is empty by A1;
A12: not g1 is identity

proof

assume g1 is identity ; :: thesis:
then g1 is Object of C by A11, CAT_6:22;
hence contradiction by A1; :: thesis:

end;

set f1 = F . g1;
A13: ( 1 in 2 & 1 is Element of 3 & 2 is Element of 3 ) by CARD_1:50, CARD_1:51, TARSKI:def 2, ENUMSET1:def 1;
then A14: [1,2] in { [o1,o2] where o1, o2 is Element of 3 : o1 in o2 } ;
then A15: [1,2] in Mor C by A4, XBOOLE_0:def 3;
reconsider g2 = [1,2] as morphism of C by A14, A4, XBOOLE_0:def 3;
A16: not g2 is identity

proof

assume g2 is identity ; :: thesis:
then g2 is Object of C by A11, CAT_6:22;
hence contradiction by A1; :: thesis:

end;

set f2 = F . g2;
A17: ( 0 in 2 & 0 is Element of 3 & 2 is Element of 3 ) by CARD_1:50, CARD_1:51, TARSKI:def 2, ENUMSET1:def 1;
then A18: [0,2] in { [o1,o2] where o1, o2 is Element of 3 : o1 in o2 } ;
reconsider g3 = [0,2] as morphism of C by A18, A4, XBOOLE_0:def 3;
set f3 = F . g3;
take F . g1 ; :: thesis:
take F . g2 ; :: thesis:
thus A19: not F . g1 is identity :: thesis:

proof

assume A20: F . g1 is identity ; :: thesis:
[0,1] in the carrier of C by A10, CAT_6:def 1;
then (id the carrier of C) . [0,1] = [0,1] by FUNCT_1:18;
then A21: (id C) . [0,1] = g1 by STRUCT_0:def 4;
G . (F . g1) is identity by A20, CAT_6:def 22, A6, CAT_6:def 25;
then (G (*) F) . g1 is identity by A6, A11, CAT_6:34;
hence contradiction by A12, A7, A11, A21, CAT_6:def 21; :: thesis:

end;

thus A22: not F . g2 is identity :: thesis:

proof

assume A23: F . g2 is identity ; :: thesis:
[1,2] in the carrier of C by A15, CAT_6:def 1;
then (id the carrier of C) . [1,2] = [1,2] by FUNCT_1:18;
then A24: (id C) . [1,2] = g2 by STRUCT_0:def 4;
G . (F . g2) is identity by A23, CAT_6:def 22, A6, CAT_6:def 25;
then (G (*) F) . g2 is identity by A6, A11, CAT_6:34;
hence contradiction by A16, A7, A11, A24, CAT_6:def 21; :: thesis:

end;

reconsider o0 = 0 as Object of C by A1, CARD_1:51, ENUMSET1:def 1;
reconsider o1 = 1 as Object of C by A1, CARD_1:51, ENUMSET1:def 1;
reconsider o2 = 2 as Object of C by A1, CARD_1:51, ENUMSET1:def 1;
A25: not C is empty by A1;
Hom (o0,o1) = {[0,1]} by A8, A2;
then A26: g1 in Hom (o0,o1) by TARSKI:def 1;
then A27: ( dom g1 = o0 & cod g1 = o1 ) by A25, CAT_7:20;
A28: ( F . (dom g1) = F . o0 & F . (cod g1) = F . o1 ) by A26, A25, CAT_7:20;
then A29: ( dom (F . g1) = F . o0 & cod (F . g1) = F . o1 ) by A6, A25, CAT_6:32;
Hom (o1,o2) = {[1,2]} by A13, A2;
then g2 in Hom (o1,o2) by TARSKI:def 1;
then A30: ( dom g2 = o1 & cod g2 = o2 ) by A25, CAT_7:20;
then A31: ( dom (F . g2) = F . o1 & cod (F . g2) = F . o2 ) by A6, A25, CAT_6:32;
thus A32: cod (F . g1) = dom (F . g2) by A29, A30, A6, A25, CAT_6:32; :: thesis:
A33: g2 |> g1 by A11, A27, A30, CAT_7:5;
then ( dom (g2 (*) g1) = dom g1 & cod (g2 (*) g1) = cod g2 ) by CAT_7:4;
then A34: g2 (*) g1 in Hom (o0,o2) by A30, A27, A11, CAT_7:20;
A35: F is multiplicative by A6, CAT_6:def 25;
A36: Hom (o0,o2) = {[0,2]} by A17, A2;
then A37: g3 = g2 (*) g1 by A34, TARSKI:def 1;
A38: F . g3 = F . (g2 (*) g1) by A36, A34, TARSKI:def 1
.= (F . g2) (*) (F . g1) by A35, A33, CAT_6:def 23 ;
for x being object holds
( x in Ob (OrdC 3) iff x in {(dom (F . g1)),(cod (F . g1)),(cod (F . g2))} )

proof

let x be object ; :: thesis:

hereby :: thesis:

assume A39: x in Ob (OrdC 3) ; :: thesis:
then reconsider o = x as Object of (OrdC 3) ;
x in Mor (OrdC 3) by A39;
then A40: o in the carrier of (OrdC 3) by CAT_6:def 1;
reconsider f = o as morphism of (OrdC 3) by A39;
A41: G is identity-preserving by A6, CAT_6:def 25;
A42: F . (G . f) = (F (*) G) . f by A6, CAT_6:34
.= (id the carrier of (OrdC 3)) . f by A7, STRUCT_0:def 4
.= (id the carrier of (OrdC 3)) . o by CAT_6:def 21
.= f by A40, FUNCT_1:18 ;
G . f is identity by A41, CAT_6:22, CAT_6:def 22;
then G . f in { f1 where f1 is morphism of C : ( f1 is identity & f1 in Mor C ) } by A11;
then G . f in {0,1,2} by A1, CARD_1:51, CAT_6:def 17;
then ( G . f = o0 or G . f = o1 or G . f = o2 ) by ENUMSET1:def 1;
then ( f = F . o0 or f = F . o1 or f = F . o2 ) by A42, A25, CAT_6:def 21;
hence x in {(dom (F . g1)),(cod (F . g1)),(cod (F . g2))} by A29, A31, ENUMSET1:def 1; :: thesis:

end;

assume x in {(dom (F . g1)),(cod (F . g1)),(cod (F . g2))} ; :: thesis:
then ( x = dom (F . g1) or x = cod (F . g1) or x = cod (F . g2) ) by ENUMSET1:def 1;
hence x in Ob (OrdC 3) ; :: thesis:

end;

hence A43: Ob (OrdC 3) = {(dom (F . g1)),(cod (F . g1)),(cod (F . g2))} by TARSKI:2; :: thesis:
for x being object holds
( x in Mor (OrdC 3) iff x in {(dom (F . g1)),(cod (F . g1)),(cod (F . g2)),(F . g1),(F . g2),((F . g2) (*) (F . g1))} )

proof

let x be object ; :: thesis:

hereby :: thesis:

assume A44: x in Mor (OrdC 3) ; :: thesis:
then A45: x in the carrier of (OrdC 3) by CAT_6:def 1;
reconsider f = x as morphism of (OrdC 3) by A44;

per cases ;

suppose f is identity ; :: thesis:

then f is Object of (OrdC 3) by CAT_6:22;
then ( x = dom (F . g1) or x = cod (F . g1) or x = cod (F . g2) ) by A43, ENUMSET1:def 1;
hence x in {(dom (F . g1)),(cod (F . g1)),(cod (F . g2)),(F . g1),(F . g2),((F . g2) (*) (F . g1))} by ENUMSET1:def 4; :: thesis:

end;

suppose A46: not f is identity ; :: thesis:

A47: (id the carrier of (OrdC 3)) . x = x by A45, FUNCT_1:18;
A48: F . (G . f) = (F (*) G) . f by A6, CAT_6:34
.= (id the carrier of (OrdC 3)) . f by A7, STRUCT_0:def 4
.= f by A47, CAT_6:def 21 ;
not G . f is identity by A48, A46, CAT_6:def 22, A6, CAT_6:def 25;
then not G . f in 3 by A1, A11, CAT_6:22;
then G . f in { [o1,o2] where o1, o2 is Element of 3 : o1 in o2 } by A4, XBOOLE_0:def 3;
then consider o1, o2 being Element of 3 such that
A49: ( G . f = [o1,o2] & o1 in o2 ) ;
A50: ( o1 = 0 or o1 = 1 or o1 = 2 ) by CARD_1:51, ENUMSET1:def 1;
( o2 = 0 or o2 = 1 or o2 = 2 ) by CARD_1:51, ENUMSET1:def 1;
hence x in {(dom (F . g1)),(cod (F . g1)),(cod (F . g2)),(F . g1),(F . g2),((F . g2) (*) (F . g1))} by A48, A38, ENUMSET1:def 4, A49, A50, CARD_1:49, CARD_1:50, TARSKI:def 1, TARSKI:def 2; :: thesis:

end;

assume x in {(dom (F . g1)),(cod (F . g1)),(cod (F . g2)),(F . g1),(F . g2),((F . g2) (*) (F . g1))} ; :: thesis:
then A51: x in {(dom (F . g1)),(cod (F . g1)),(cod (F . g2))} \/ {(F . g1),(F . g2),((F . g2) (*) (F . g1))} by ENUMSET1:13;

per cases by A51, A43, XBOOLE_0:def 3;

suppose x in Ob (OrdC 3) ; :: thesis:

hence x in Mor (OrdC 3) ; :: thesis:

end;

suppose x in {(F . g1),(F . g2),((F . g2) (*) (F . g1))} ; :: thesis:

then ( x = F . g1 or x = F . g2 or x = (F . g2) (*) (F . g1) ) by ENUMSET1:def 1;
hence x in Mor (OrdC 3) ; :: thesis:

end;

hence Mor (OrdC 3) = {(dom (F . g1)),(cod (F . g1)),(cod (F . g2)),(F . g1),(F . g2),((F . g2) (*) (F . g1))} by TARSKI:2; :: thesis:
0 in 2 by CARD_1:50, TARSKI:def 2;
then [0,2] in { [o1,o2] where o1, o2 is Element of 3 : o1 in o2 } by A8, A13;
then A52: [0,2] in Mor C by A4, XBOOLE_0:def 3;
A53: F . g2 |> F . g1 by A33, A35, CAT_6:def 23;
A54: F . (g2 (*) g1) = (F . g2) (*) (F . g1) by A35, A33, CAT_6:def 23;
A55: not g2 (*) g1 is identity

proof

assume g2 (*) g1 is identity ; :: thesis:
then g2 (*) g1 is Object of C by A11, CAT_6:22;
hence contradiction by A1, A36, A34, TARSKI:def 1; :: thesis:

end;

A56: not (F . g2) (*) (F . g1) is identity

proof

assume A57: (F . g2) (*) (F . g1) is identity ; :: thesis:
[0,2] in the carrier of C by A52, CAT_6:def 1;
then (id the carrier of C) . [0,2] = [0,2] by FUNCT_1:18;
then A58: (id C) . [0,2] = g2 (*) g1 by A37, STRUCT_0:def 4;
G . (F . (g2 (*) g1)) is identity by A54, A57, CAT_6:def 22, A6, CAT_6:def 25;
then (G (*) F) . (g2 (*) g1) is identity by A6, A11, CAT_6:34;
hence contradiction by A55, A37, A7, A11, A58, CAT_6:def 21; :: thesis:

end;

dom (F . g1) in Ob (OrdC 3) ;
then reconsider o11 = dom (F . g1) as morphism of (OrdC 3) ;
cod (F . g1) in Ob (OrdC 3) ;
then reconsider o22 = cod (F . g1) as morphism of (OrdC 3) ;
cod (F . g2) in Ob (OrdC 3) ;
then reconsider o33 = cod (F . g2) as morphism of (OrdC 3) ;
A59: ( o11 is identity & o22 is identity & o33 is identity ) by CAT_6:22;
A60: F is bijective by Th9, A6, A7, CAT_7:def 19;
dom F = the carrier of C by FUNCT_2:def 1;
then A61: dom F = Mor C by CAT_6:def 1;
A62: ( o0 in Ob C & o1 in Ob C & o2 in Ob C ) by A1;
A63: dom (F . g1) <> cod (F . g1) by A29, A60, A62, A61, FUNCT_1:def 4;
A64: dom (F . g1) <> cod (F . g2) by A28, A31, A60, A62, A61, FUNCT_1:def 4, A6, A25, CAT_6:32;
A65: cod (F . g1) <> cod (F . g2) by A28, A31, A60, A62, A61, FUNCT_1:def 4, A6, A25, CAT_6:32;
A66: F . g1 <> (F . g2) (*) (F . g1) by A65, A53, CAT_7:4;
F . g2 <> (F . g2) (*) (F . g1) by A29, A60, A62, A61, FUNCT_1:def 4, A32, A53, CAT_7:4;
hence dom (F . g1), cod (F . g1), cod (F . g2),F . g1,F . g2,(F . g2) (*) (F . g1) are_mutually_distinct by A19, A22, A63, A56, A59, A66, A64, A65, ZFMISC_1:def 8; :: thesis: