take A = RelStr(# {{}},(id {{}}) #); :: thesis: ( A is strict & not A is empty & A is constituted-Functions )
thus ( A is strict & not A is empty ) ; :: 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