per cases ( x nin dom C or x in dom C ) ;

suppose x nin dom C ; :: thesis: ( C . x is segmental & C . x is Function-like & C . x is Relation-like )

hence ( C . x is segmental & C . x is Function-like & C . x is Relation-like ) by FUNCT_1:def 2; :: thesis: verum

end;

suppose x in dom C ; :: thesis: ( C . x is segmental & C . x is Function-like & C . x is Relation-like )

hence ( C . x is segmental & C . x is Function-like & C . x is Relation-like ) by Def14; :: thesis: verum

end;

end;