let
S
be
full
SubNetStr
of
N
;
:: thesis:
S
is
transitive
S
is
full
SubRelStr
of
N
by
YELLOW_6:def 7
;
hence
S
is
transitive
;
:: thesis:
verum