deffunc H1( Element of NAT ) -> Element of FinTrees HP-WFF = root-tree (prop $1);
defpred S1[ Element of HP-WFF , Element of HP-WFF , set , set , set ] means ( ( $3 is DecoratedTree of HP-WFF & $4 is DecoratedTree of HP-WFF implies ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = $3 & q9 = $4 & $5 = ($1 => $2) -tree (p9,q9) ) ) & ( ( not $3 is DecoratedTree of HP-WFF or not $4 is DecoratedTree of HP-WFF ) implies $5 = {} ) );
defpred S2[ Element of HP-WFF , Element of HP-WFF , set , set , set ] means ( ( $3 is DecoratedTree of HP-WFF & $4 is DecoratedTree of HP-WFF implies ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = $3 & q9 = $4 & $5 = ($1 '&' $2) -tree (p9,q9) ) ) & ( ( not $3 is DecoratedTree of HP-WFF or not $4 is DecoratedTree of HP-WFF ) implies $5 = {} ) );
A1: for p, q being Element of HP-WFF
for a, b being set ex c being set st S2[p,q,a,b,c]
proof
let p, q be Element of HP-WFF ; :: thesis: for a, b being set ex c being set st S2[p,q,a,b,c]
let a, b be set ; :: thesis: ex c being set st S2[p,q,a,b,c]
per cases ( ( a is DecoratedTree of HP-WFF & b is DecoratedTree of HP-WFF ) or not a is DecoratedTree of HP-WFF or not b is DecoratedTree of HP-WFF ) ;
suppose that A2: a is DecoratedTree of HP-WFF and
A3: b is DecoratedTree of HP-WFF ; :: thesis: ex c being set st S2[p,q,a,b,c]
reconsider q9 = b as DecoratedTree of HP-WFF by A3;
reconsider p9 = a as DecoratedTree of HP-WFF by A2;
take (p '&' q) -tree (p9,q9) ; :: thesis: S2[p,q,a,b,(p '&' q) -tree (p9,q9)]
thus S2[p,q,a,b,(p '&' q) -tree (p9,q9)] ; :: thesis: verum
end;
suppose ( not a is DecoratedTree of HP-WFF or not b is DecoratedTree of HP-WFF ) ; :: thesis: ex c being set st S2[p,q,a,b,c]
hence ex c being set st S2[p,q,a,b,c] ; :: thesis: verum
end;
end;
end;
A4: for p, q being Element of HP-WFF
for a, b being set ex d being set st S1[p,q,a,b,d]
proof
let p, q be Element of HP-WFF ; :: thesis: for a, b being set ex d being set st S1[p,q,a,b,d]
let a, b be set ; :: thesis: ex d being set st S1[p,q,a,b,d]
per cases ( ( a is DecoratedTree of HP-WFF & b is DecoratedTree of HP-WFF ) or not a is DecoratedTree of HP-WFF or not b is DecoratedTree of HP-WFF ) ;
suppose that A5: a is DecoratedTree of HP-WFF and
A6: b is DecoratedTree of HP-WFF ; :: thesis: ex d being set st S1[p,q,a,b,d]
reconsider q9 = b as DecoratedTree of HP-WFF by A6;
reconsider p9 = a as DecoratedTree of HP-WFF by A5;
take (p => q) -tree (p9,q9) ; :: thesis: S1[p,q,a,b,(p => q) -tree (p9,q9)]
thus S1[p,q,a,b,(p => q) -tree (p9,q9)] ; :: thesis: verum
end;
suppose ( not a is DecoratedTree of HP-WFF or not b is DecoratedTree of HP-WFF ) ; :: thesis: ex d being set st S1[p,q,a,b,d]
hence ex d being set st S1[p,q,a,b,d] ; :: thesis: verum
end;
end;
end;
A7: for p, q being Element of HP-WFF
for a, b, c, d being set st S1[p,q,a,b,c] & S1[p,q,a,b,d] holds
c = d ;
A8: for p, q being Element of HP-WFF
for a, b, c, d being set st S2[p,q,a,b,c] & S2[p,q,a,b,d] holds
c = d ;
consider M being ManySortedSet of HP-WFF such that
A9: M . VERUM = root-tree VERUM and
A10: for n being Element of NAT holds M . (prop n) = H1(n) and
A11: for p, q being Element of HP-WFF holds
( S2[p,q,M . p,M . q,M . (p '&' q)] & S1[p,q,M . p,M . q,M . (p => q)] ) from HILBERT2:sch 3(A1, A4, A8, A7);
 take M ; :: thesis: ( M . VERUM = root-tree VERUM & ( for n being Element of NAT holds M . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = M . p & q9 = M . q & M . (p '&' q) = (p '&' q) -tree (p9,q9) & M . (p => q) = (p => q) -tree (p9,q9) ) ) )
thus M . VERUM = root-tree VERUM by A9; :: thesis: ( ( for n being Element of NAT holds M . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = M . p & q9 = M . q & M . (p '&' q) = (p '&' q) -tree (p9,q9) & M . (p => q) = (p => q) -tree (p9,q9) ) ) )
thus for n being Element of NAT holds M . (prop n) = root-tree (prop n) by A10; :: thesis: for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = M . p & q9 = M . q & M . (p '&' q) = (p '&' q) -tree (p9,q9) & M . (p => q) = (p => q) -tree (p9,q9) )
let p, q be Element of HP-WFF ; :: thesis: ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = M . p & q9 = M . q & M . (p '&' q) = (p '&' q) -tree (p9,q9) & M . (p => q) = (p => q) -tree (p9,q9) )
A12: ( S2[p,q,M . p,M . q,M . (p '&' q)] & S1[p,q,M . p,M . q,M . (p => q)] ) by A11;
defpred S3[ Element of HP-WFF ] means M . $1 is DecoratedTree of HP-WFF ;
A13: for r, s being Element of HP-WFF st S3[r] & S3[s] holds
( S3[r '&' s] & S3[r => s] )
proof
let r, s be Element of HP-WFF ; :: thesis: ( S3[r] & S3[s] implies ( S3[r '&' s] & S3[r => s] ) )
assume A14: ( M . r is DecoratedTree of HP-WFF & M . s is DecoratedTree of HP-WFF ) ; :: thesis: ( S3[r '&' s] & S3[r => s] )
S2[r,s,M . r,M . s,M . (r '&' s)] by A11;
hence M . (r '&' s) is DecoratedTree of HP-WFF by A14; :: thesis: S3[r => s]
S1[r,s,M . r,M . s,M . (r => s)] by A11;
hence S3[r => s] by A14; :: thesis: verum
end;
A15: for n being Element of NAT holds S3[ prop n]
proof
let n be Element of NAT ; :: thesis: S3[ prop n]
M . (prop n) = root-tree (prop n) by A10;
hence S3[ prop n] ; :: thesis: verum
end;
A16: S3[ VERUM ] by A9;
for p being Element of HP-WFF holds S3[p] from HILBERT2:sch 2(A16, A15, A13);
 hence ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = M . p & q9 = M . q & M . (p '&' q) = (p '&' q) -tree (p9,q9) & M . (p => q) = (p => q) -tree (p9,q9) ) by A12; :: thesis: verum