let S be non empty SubRelStr of T; :: thesis: S is constituted-Functions
let a be Element of S; :: according to MONOID_0:def 1 :: thesis: a is set
the carrier of S c= the carrier of T by YELLOW_0:def 13;
hence a is set ; :: thesis: verum