deffunc H₆( Element of QC-WFF , Subset of V) -> Subset of V = $2;
deffunc H₇( Subset of V, Subset of V) -> Element of bool V = $1 \/ $2;
deffunc H₈( Subset of V) -> Subset of V = $1;
deffunc H₉( Element of QC-WFF ) -> Subset of V = variables_in (the_arguments_of $1),V;
thus ( ex d being Subset of V ex F being Function of QC-WFF ,(bool V) st
( d = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of V holds
( ( p = VERUM implies F . p = {} V ) & ( p is atomic implies F . p = H₉(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H₈(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H₇(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H₆(p,d1) ) ) ) ) & ( for x1, x2 being Subset of V st ex F being Function of QC-WFF ,(bool V) st
( x1 = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of V holds
( ( p = VERUM implies F . p = {} V ) & ( p is atomic implies F . p = H₉(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H₈(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H₇(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H₆(p,d1) ) ) ) ) & ex F being Function of QC-WFF ,(bool V) st
( x2 = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of V holds
( ( p = VERUM implies F . p = {} V ) & ( p is atomic implies F . p = H₉(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H₈(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H₇(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H₆(p,d1) ) ) ) ) holds
x1 = x2 ) ) from QC_LANG3:sch 2(); :: thesis: verum