let p be Element of HP-WFF ; :: thesis: ( p is pseudo-canonical implies p is classical )

assume AA: p is pseudo-canonical ; :: thesis: p is classical

defpred S_{2}[ Function] means ex x being set st x is_a_fixpoint_of c_{1};

assume not p is classical ; :: thesis: contradiction

then consider v being SetValuation0 such that

B0: SetVal0 (v,p) = {} ;

set P = v tohilbperm ;

set V = v tohilbval ;

fixpoints (Perm ((v tohilbperm),p)) = {} by Lm100, B0;

then not S_{2}[ Perm ((v tohilbperm),p)]
by FOMODEL0:69;

hence contradiction by AA, HILBERT3:def 8; :: thesis: verum

assume AA: p is pseudo-canonical ; :: thesis: p is classical

defpred S

assume not p is classical ; :: thesis: contradiction

then consider v being SetValuation0 such that

B0: SetVal0 (v,p) = {} ;

set P = v tohilbperm ;

set V = v tohilbval ;

fixpoints (Perm ((v tohilbperm),p)) = {} by Lm100, B0;

then not S

hence contradiction by AA, HILBERT3:def 8; :: thesis: verum