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

proof

assume g is identity ; :: thesis: contradiction
then g is Object of C by A10, CAT_6:22;
hence contradiction by A1; :: thesis: verum

end;

set f = F . g;
take F . g ; :: thesis: ( not F . g is identity & Ob (OrdC 2) = {(dom (F . g)),(cod (F . g))} & Mor (OrdC 2) = {(dom (F . g)),(cod (F . g)),(F . g)} & dom (F . g), cod (F . g),F . g are_mutually_distinct )
thus A12: not F . g is identity :: thesis: ( Ob (OrdC 2) = {(dom (F . g)),(cod (F . g))} & Mor (OrdC 2) = {(dom (F . g)),(cod (F . g)),(F . g)} & dom (F . g), cod (F . g),F . g are_mutually_distinct )

proof

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

end;

card (Ob (OrdC 2)) = card 2 by A1, A5, Th14;
then consider x, y being object such that
A15: ( x <> y & Ob (OrdC 2) = {x,y} ) by CARD_2:60;
A16: ( dom (F . g) = x or dom (F . g) = y ) by A15, TARSKI:def 2;
A17: dom (F . g) <> cod (F . g)

proof

assume dom (F . g) = cod (F . g) ; :: thesis: contradiction
then A18: F . g in Hom ((dom (F . g)),(dom (F . g))) ;
id- (dom (F . g)) in Hom ((dom (F . g)),(dom (F . g))) by Def3;
hence contradiction by A12, A18, Def12; :: thesis: verum

end;

hence A19: Ob (OrdC 2) = {(dom (F . g)),(cod (F . g))} by A15, A16, TARSKI:def 2; :: thesis: ( Mor (OrdC 2) = {(dom (F . g)),(cod (F . g)),(F . g)} & dom (F . g), cod (F . g),F . g are_mutually_distinct )
for x being object holds
( x in Mor (OrdC 2) iff x in {(dom (F . g)),(cod (F . g)),(F . g)} )

proof

let x be object ; :: thesis: ( x in Mor (OrdC 2) iff x in {(dom (F . g)),(cod (F . g)),(F . g)} )

hereby :: thesis: ( x in {(dom (F . g)),(cod (F . g)),(F . g)} implies x in Mor (OrdC 2) )

assume A20: x in Mor (OrdC 2) ; :: thesis: x in {(dom (F . g)),(cod (F . g)),(F . g)}
then A21: x in the carrier of (OrdC 2) by CAT_6:def 1;
reconsider f1 = x as morphism of (OrdC 2) by A20;

per cases ( f1 is identity or not f1 is identity ) ;

suppose f1 is identity ; :: thesis: x in {(dom (F . g)),(cod (F . g)),(F . g)}

then f1 is Object of (OrdC 2) by CAT_6:22;
then ( x = dom (F . g) or x = cod (F . g) ) by A19, TARSKI:def 2;
hence x in {(dom (F . g)),(cod (F . g)),(F . g)} by ENUMSET1:def 1; :: thesis: verum

end;

suppose A22: not f1 is identity ; :: thesis: x in {(dom (F . g)),(cod (F . g)),(F . g)}

A23: (id the carrier of (OrdC 2)) . x = x by A21, FUNCT_1:18;
A24: F . (G . f1) = (F (*) G) . f1 by A6, CAT_6:34
.= (id the carrier of (OrdC 2)) . f1 by A7, STRUCT_0:def 4
.= f1 by A23, CAT_6:def 21 ;
not G . f1 is identity by A24, A22, CAT_6:def 22, A6, CAT_6:def 25;
then not G . f1 in 2 by A1, A10, CAT_6:22;
then G . f1 in { [o1,o2] where o1, o2 is Element of 2 : o1 in o2 } by A3, XBOOLE_0:def 3;
then consider o1, o2 being Element of 2 such that
A25: ( G . f1 = [o1,o2] & o1 in o2 ) ;
A26: ( o1 = 0 or o1 = 1 ) by CARD_1:50, TARSKI:def 2;
( o2 = 0 or o2 = 1 ) by CARD_1:50, TARSKI:def 2;
hence x in {(dom (F . g)),(cod (F . g)),(F . g)} by A25, A26, A24, ENUMSET1:def 1, CARD_1:49, TARSKI:def 1; :: thesis: verum

end;

end;

end;

assume x in {(dom (F . g)),(cod (F . g)),(F . g)} ; :: thesis: x in Mor (OrdC 2)
then A27: x in {(dom (F . g)),(cod (F . g))} \/ {(F . g)} by ENUMSET1:3;

per cases ( x in Ob (OrdC 2) or x in {(F . g)} ) by A27, A19, XBOOLE_0:def 3;

suppose x in Ob (OrdC 2) ; :: thesis: x in Mor (OrdC 2)

hence x in Mor (OrdC 2) ; :: thesis: verum

end;

suppose x in {(F . g)} ; :: thesis: x in Mor (OrdC 2)

then x = F . g by TARSKI:def 1;
hence x in Mor (OrdC 2) ; :: thesis: verum

end;

end;

end;

hence Mor (OrdC 2) = {(dom (F . g)),(cod (F . g)),(F . g)} by TARSKI:2; :: thesis: dom (F . g), cod (F . g),F . g are_mutually_distinct
( dom (F . g) <> cod (F . g) & dom (F . g) <> F . g & cod (F . g) <> F . g ) by A12, A17, CAT_6:22;
hence dom (F . g), cod (F . g),F . g are_mutually_distinct by ZFMISC_1:def 5; :: thesis: verum