:: BVFUNC_4  semantic presentation begin  



theorem :: BVFUNC_4:1 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_bvfunc_1 :::"'<'"::: )  (Set (Set (Var "b"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "c"))))) "holds"  (Bool (Set (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "b")))  ($#r1_bvfunc_1 :::"'<'"::: )  (Set (Var "c"))))) ; 
 
theorem :: BVFUNC_4:2 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) )  "st" (Bool (Bool (Set (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "b")))  ($#r1_bvfunc_1 :::"'<'"::: )  (Set (Var "c")))) "holds"  (Bool (Set (Var "a"))  ($#r1_bvfunc_1 :::"'<'"::: )  (Set (Set (Var "b"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "c")))))) ; 
 
theorem :: BVFUNC_4:3 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds"  (Bool (Set (Set (Var "a"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set  "(" (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "b")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Var "a"))))) ; 
 
theorem :: BVFUNC_4:4 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds"  (Bool (Set (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set  "(" (Set (Var "a"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "b")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Var "a"))))) ; 
 
theorem :: BVFUNC_4:5 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds"  (Bool (Set (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "a")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k11_bvfunc_1 :::"O_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_4:6 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds"  (Bool (Set (Set (Var "a"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "a")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_4:7 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds"  (Bool (Set (Set (Var "a"))  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set (Var "b")))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "b")) ")" )  ($#k2_bvfunc_1 :::"'&'"::: )  (Set  "(" (Set (Var "b"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "a")) ")" ))))) ; 
 
theorem :: BVFUNC_4:8 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds"  (Bool (Set (Set (Var "a"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "b")))  ($#r2_funct_2 :::"="::: )  (Set (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "a")) ")" )  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "b")))))) ; 
 
theorem :: BVFUNC_4:9 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_bvfunc_1 :::"'xor'"::: )  (Set (Var "b")))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "a")) ")" )  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "b")) ")" )  ($#k5_bvfunc_1 :::"'or'"::: )  (Set  "(" (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "b")) ")" ) ")" ))))) ; 
 
theorem :: BVFUNC_4:10 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds"   (Bool  "("  (Bool (Set (Set (Var "a"))  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set (Var "b")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))) "iff" (Bool  "("  (Bool (Set (Set (Var "a"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "b")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))) & (Bool (Set (Set (Var "b"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "a")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y"))))  ")" )  ")" ))) ; 
 
theorem :: BVFUNC_4:11 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) )  "st" (Bool (Bool (Set (Set (Var "a"))  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set (Var "b")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y"))))) "holds"  (Bool (Set (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "a")) ")" )  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "b")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_4:12 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) )  "st" (Bool (Bool (Set (Set (Var "a"))  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set (Var "b")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))) & (Bool (Set (Set (Var "c"))  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set (Var "d")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "c")) ")" )  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set  "(" (Set (Var "b"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "d")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_4:13 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) )  "st" (Bool (Bool (Set (Set (Var "a"))  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set (Var "b")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))) & (Bool (Set (Set (Var "c"))  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set (Var "d")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "c")) ")" )  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set  "(" (Set (Var "b"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "d")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_4:14 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) )  "st" (Bool (Bool (Set (Set (Var "a"))  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set (Var "b")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))) & (Bool (Set (Set (Var "c"))  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set (Var "d")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "c")) ")" )  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set  "(" (Set (Var "b"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "d")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_4:15 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) )  "st" (Bool (Bool (Set (Set (Var "a"))  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set (Var "b")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))) & (Bool (Set (Set (Var "c"))  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set (Var "d")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set (Var "c")) ")" )  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set  "(" (Set (Var "b"))  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set (Var "d")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 begin  
theorem :: BVFUNC_4:16 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) )  (Bool  "for" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_bvfunc_2 :::"PARTITIONS"::: )  (Set (Var "Y")) ")" )  (Bool  "for" (Set (Var "PA")) "being"    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set (Var "Y")) "holds"  (Bool (Set   ($#k6_bvfunc_2 :::"All"::: )   "(" (Set  "(" (Set (Var "a"))  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )  ($#r2_funct_2 :::"="::: )  (Set (Set  "("  ($#k6_bvfunc_2 :::"All"::: )   "(" (Set  "(" (Set (Var "a"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")"  ")" )  ($#k2_bvfunc_1 :::"'&'"::: )  (Set  "("  ($#k6_bvfunc_2 :::"All"::: )   "(" (Set  "(" (Set (Var "b"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "a")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")"  ")" ))))))) ; 
 
theorem :: BVFUNC_4:17 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) )  (Bool  "for" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_bvfunc_2 :::"PARTITIONS"::: )  (Set (Var "Y")) ")" )  (Bool  "for" (Set (Var "PA")) "," (Set (Var "PB")) "being"    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set (Var "Y")) "holds"  (Bool (Set   ($#k6_bvfunc_2 :::"All"::: )   "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )  ($#r1_bvfunc_1 :::"'<'"::: )  (Set   ($#k7_bvfunc_2 :::"Ex"::: )   "(" (Set (Var "a")) "," (Set (Var "PB")) "," (Set (Var "G")) ")" )))))) ; 
 
theorem :: BVFUNC_4:18 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "u")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) )  (Bool  "for" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_bvfunc_2 :::"PARTITIONS"::: )  (Set (Var "Y")) ")" )  (Bool  "for" (Set (Var "PA")) "being"    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set (Var "Y"))  "st" (Bool (Bool (Set (Set (Var "a"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "u")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y"))))) "holds"  (Bool (Set (Set  "("  ($#k6_bvfunc_2 :::"All"::: )   "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")"  ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "u")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))))) ; 
 
theorem :: BVFUNC_4:19 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) )  (Bool  "for" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_bvfunc_2 :::"PARTITIONS"::: )  (Set (Var "Y")) ")" )  (Bool  "for" (Set (Var "PA")) "being"    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "u"))  ($#r3_bvfunc_2 :::"is_independent_of"::: )  (Set (Var "PA")) "," (Set (Var "G")))) "holds"  (Bool (Set   ($#k7_bvfunc_2 :::"Ex"::: )   "(" (Set (Var "u")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )  ($#r1_bvfunc_1 :::"'<'"::: )  (Set (Var "u"))))))) ; 
 
theorem :: BVFUNC_4:20 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) )  (Bool  "for" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_bvfunc_2 :::"PARTITIONS"::: )  (Set (Var "Y")) ")" )  (Bool  "for" (Set (Var "PA")) "being"    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "u"))  ($#r3_bvfunc_2 :::"is_independent_of"::: )  (Set (Var "PA")) "," (Set (Var "G")))) "holds"  (Bool (Set (Var "u"))  ($#r1_bvfunc_1 :::"'<'"::: )  (Set   ($#k6_bvfunc_2 :::"All"::: )   "(" (Set (Var "u")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; 
 
theorem :: BVFUNC_4:21 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) )  (Bool  "for" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_bvfunc_2 :::"PARTITIONS"::: )  (Set (Var "Y")) ")" )  (Bool  "for" (Set (Var "PA")) "," (Set (Var "PB")) "being"    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "u"))  ($#r3_bvfunc_2 :::"is_independent_of"::: )  (Set (Var "PB")) "," (Set (Var "G")))) "holds"  (Bool (Set   ($#k6_bvfunc_2 :::"All"::: )   "(" (Set (Var "u")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )  ($#r1_bvfunc_1 :::"'<'"::: )  (Set   ($#k6_bvfunc_2 :::"All"::: )   "(" (Set (Var "u")) "," (Set (Var "PB")) "," (Set (Var "G")) ")" )))))) ; 
 
theorem :: BVFUNC_4:22 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) )  (Bool  "for" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_bvfunc_2 :::"PARTITIONS"::: )  (Set (Var "Y")) ")" )  (Bool  "for" (Set (Var "PA")) "," (Set (Var "PB")) "being"    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "u"))  ($#r3_bvfunc_2 :::"is_independent_of"::: )  (Set (Var "PA")) "," (Set (Var "G")))) "holds"  (Bool (Set   ($#k7_bvfunc_2 :::"Ex"::: )   "(" (Set (Var "u")) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )  ($#r1_bvfunc_1 :::"'<'"::: )  (Set   ($#k7_bvfunc_2 :::"Ex"::: )   "(" (Set (Var "u")) "," (Set (Var "PB")) "," (Set (Var "G")) ")" )))))) ; 
 
theorem :: BVFUNC_4:23 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) )  (Bool  "for" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_bvfunc_2 :::"PARTITIONS"::: )  (Set (Var "Y")) ")" )  (Bool  "for" (Set (Var "PA")) "being"    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set (Var "Y")) "holds"  (Bool (Set   ($#k6_bvfunc_2 :::"All"::: )   "(" (Set  "(" (Set (Var "a"))  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )  ($#r1_bvfunc_1 :::"'<'"::: )  (Set (Set  "("  ($#k6_bvfunc_2 :::"All"::: )   "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")"  ")" )  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set  "("  ($#k6_bvfunc_2 :::"All"::: )   "(" (Set (Var "b")) "," (Set (Var "PA")) "," (Set (Var "G")) ")"  ")" ))))))) ; 
 
theorem :: BVFUNC_4:24 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) )  (Bool  "for" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_bvfunc_2 :::"PARTITIONS"::: )  (Set (Var "Y")) ")" )  (Bool  "for" (Set (Var "PA")) "being"    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set (Var "Y")) "holds"  (Bool (Set   ($#k6_bvfunc_2 :::"All"::: )   "(" (Set  "(" (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "b")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )  ($#r1_bvfunc_1 :::"'<'"::: )  (Set (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set  "("  ($#k6_bvfunc_2 :::"All"::: )   "(" (Set (Var "b")) "," (Set (Var "PA")) "," (Set (Var "G")) ")"  ")" ))))))) ; 
 
theorem :: BVFUNC_4:25 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "u")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) )  (Bool  "for" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_bvfunc_2 :::"PARTITIONS"::: )  (Set (Var "Y")) ")" )  (Bool  "for" (Set (Var "PA")) "being"    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set (Var "Y")) "holds"  (Bool (Set (Set  "("  ($#k6_bvfunc_2 :::"All"::: )   "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")"  ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "u")))  ($#r1_bvfunc_1 :::"'<'"::: )  (Set   ($#k7_bvfunc_2 :::"Ex"::: )   "(" (Set  "(" (Set (Var "a"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "u")) ")" ) "," (Set (Var "PA")) "," (Set (Var "G")) ")" )))))) ; 
 
theorem :: BVFUNC_4:26 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) )  (Bool  "for" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_bvfunc_2 :::"PARTITIONS"::: )  (Set (Var "Y")) ")" )  (Bool  "for" (Set (Var "PA")) "being"    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set (Var "Y"))  "st" (Bool (Bool (Set (Set (Var "a"))  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set (Var "b")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y"))))) "holds"  (Bool (Set (Set  "("  ($#k6_bvfunc_2 :::"All"::: )   "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")"  ")" )  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set  "("  ($#k6_bvfunc_2 :::"All"::: )   "(" (Set (Var "b")) "," (Set (Var "PA")) "," (Set (Var "G")) ")"  ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))))) ; 
 
theorem :: BVFUNC_4:27 (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) )  (Bool  "for" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_bvfunc_2 :::"PARTITIONS"::: )  (Set (Var "Y")) ")" )  (Bool  "for" (Set (Var "PA")) "being"    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set (Var "Y"))  "st" (Bool (Bool (Set (Set (Var "a"))  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set (Var "b")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y"))))) "holds"  (Bool (Set (Set  "("  ($#k7_bvfunc_2 :::"Ex"::: )   "(" (Set (Var "a")) "," (Set (Var "PA")) "," (Set (Var "G")) ")"  ")" )  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set  "("  ($#k7_bvfunc_2 :::"Ex"::: )   "(" (Set (Var "b")) "," (Set (Var "PA")) "," (Set (Var "G")) ")"  ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))))) ;