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₂[ Function] means ex x being set st x is_a_fixpoint_of c₁;
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₂[ Perm ((v tohilbperm),p)] by FOMODEL0:69;
hence contradiction by AA, HILBERT3:def 8; :: thesis: verum