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
( a in the carrier of S & the carrier of S c= the carrier of T ) by YELLOW_0:def 13;
then a is Element of T ;
hence a is set ; :: thesis: verum