per
cases
(
C
is
empty
or not
C
is
empty
)
;
suppose
C
is
empty
;
:: thesis:
id-
a
is
identity
hence
id-
a
is
identity
by
CAT_6:10
;
:: thesis:
verum
end;
suppose
A1
: not
C
is
empty
;
:: thesis:
id-
a
is
identity
id-
a
=
a
by
CAT_6:def 20
;
hence
id-
a
is
identity
by
A1
,
CAT_6:22
;
:: thesis:
verum
end;
end;