thus ( X is categorial implies for x being Element of X holds x is Category ) by Def4; :: thesis: ( ( for x being Element of X holds x is Category ) implies X is categorial )
assume A1: for x being Element of X holds x is Category ; :: thesis: X is categorial
let x be set ; :: according to CAT_5:def 4 :: thesis: ( x in X implies x is Category )
thus ( x in X implies x is Category ) by A1; :: thesis: verum