take A = 1-sorted(# {{}} #); :: thesis: ( not A is empty & A is constituted-Functions )
thus not the carrier of A is empty ; :: according to STRUCT_0:def 1 :: thesis: A is constituted-Functions
let a be Element of A; :: according to MONOID_0:def 1 :: thesis: a is set
thus a is set ; :: thesis: verum