defpred S_{1}[ Element of HP-WFF ] means not (SetVal V) . V is empty ;

A1: for n being Element of NAT holds S_{1}[ prop n]
_{1}[r] & S_{1}[s] holds

( S_{1}[r '&' s] & S_{1}[r => s] )
_{1}[ VERUM ]
by Def2;

for r being Element of HP-WFF holds S_{1}[r]
from HILBERT2:sch 2(A5, A1, A2);

hence not SetVal (V,p) is empty ; :: thesis: verum

A1: for n being Element of NAT holds S

proof

A2:
for r, s being Element of HP-WFF st S
let n be Element of NAT ; :: thesis: S_{1}[ prop n]

(SetVal V) . (prop n) = V . n by Def2;

hence S_{1}[ prop n]
; :: thesis: verum

end;(SetVal V) . (prop n) = V . n by Def2;

hence S

( S

proof

A5:
S
let r, s be Element of HP-WFF ; :: thesis: ( S_{1}[r] & S_{1}[s] implies ( S_{1}[r '&' s] & S_{1}[r => s] ) )

assume that

A3: not (SetVal V) . r is empty and

A4: not (SetVal V) . s is empty ; :: thesis: ( S_{1}[r '&' s] & S_{1}[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_{1}[r => s]

(SetVal V) . (r => s) = Funcs (((SetVal V) . r),((SetVal V) . s)) by Def2;

hence S_{1}[r => s]
by A4; :: thesis: verum

end;assume that

A3: not (SetVal V) . r is empty and

A4: not (SetVal V) . s is empty ; :: thesis: ( 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

(SetVal V) . (r => s) = Funcs (((SetVal V) . r),((SetVal V) . s)) by Def2;

hence S

for r being Element of HP-WFF holds S

hence not SetVal (V,p) is empty ; :: thesis: verum