let P be non empty ProofSystem ; :: thesis: for a being object holds
( P |- a iff for X being P -closed set holds a in X )
let a be object ; :: thesis: ( P |- a iff for X being P -closed set holds a in X )
set A = the Axioms of P;
thus ( P |- a implies for X being P -closed set holds a in X ) by Th65; :: thesis: ( ( for X being P -closed set holds a in X ) implies P |- a )
assume for X being P -closed set holds a in X ; :: thesis: P |- a
then a in Theorems P ;
hence P |- a by Def30r; :: thesis: verum