let X be set ; :: thesis: SubFuncs X c= X
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in SubFuncs X or x in X )
thus ( not x in SubFuncs X or x in X ) by Def1; :: thesis: verum