deffunc H₁( Element of NAT ) -> set = V . $1;
consider M being ManySortedSet of HP-WFF such that
A1: ( M . VERUM = 1 & ( for n being Element of NAT holds M . (prop n) = H₁(n) ) & ( for p, q being Element of HP-WFF holds
( M . (p '&' q) = [:(M . p),(M . q):] & M . (p => q) = Funcs ((M . p),(M . q)) ) ) ) from HILBERT2:sch 4();
take M ; :: thesis: ( M . VERUM = 1 & ( for n being Element of NAT holds M . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( M . (p '&' q) = [:(M . p),(M . q):] & M . (p => q) = Funcs ((M . p),(M . q)) ) ) )
thus ( M . VERUM = 1 & ( for n being Element of NAT holds M . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( M . (p '&' q) = [:(M . p),(M . q):] & M . (p => q) = Funcs ((M . p),(M . q)) ) ) ) by A1; :: thesis: verum