scheme :: HILBERT2:sch 4
HPMSSLambda{ F1() -> set , F2( Element of NAT ) -> set , F3( set , set ) -> set , F4( set , set ) -> set } :
ex M being ManySortedSet of HP-WFF st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF holds
( M . (p '&' q) = F3((M . p),(M . q)) & M . (p => q) = F4((M . p),(M . q)) ) ) )