defpred S₁[ Element of HP-WFF ] means not (SetVal V) . V is empty ;
A1: for n being Element of NAT holds S₁[ prop n]

proof

let n be Element of NAT ; :: thesis: S₁[ prop n]
(SetVal V) . (prop n) = V . n by Def2;
hence S₁[ prop n] ; :: thesis: verum

end;

A2: for r, s being Element of HP-WFF st S₁[r] & S₁[s] holds
( S₁[r '&' s] & S₁[r => s] )

proof

let r, s be Element of HP-WFF ; :: thesis: ( S₁[r] & S₁[s] implies ( S₁[r '&' s] & S₁[r => s] ) )
assume that
A3: not (SetVal V) . r is empty and
A4: not (SetVal V) . s is empty ; :: thesis: ( S₁[r '&' s] & S₁[r => s] )
(SetVal V) . (r '&' s) = [:((SetVal V) . r),((SetVal V) . s):] by Def2;
hence not (SetVal V) . (r '&' s) is empty by A3, A4; :: thesis: S₁[r => s]
(SetVal V) . (r => s) = Funcs (((SetVal V) . r),((SetVal V) . s)) by Def2;
hence S₁[r => s] by A4; :: thesis: verum

end;

A5: S₁[ VERUM ] by Def2;
for r being Element of HP-WFF holds S₁[r] from HILBERT2:sch 2(A5, A1, A2);
hence not SetVal (V,p) is empty ; :: thesis: verum