:: BVFUNC_6  semantic presentation begin  



theorem :: BVFUNC_6: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")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds"  (Bool (Set (Set (Var "a"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set (Var "b"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "b")) ")" ) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6: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")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "b")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set  "(" (Set (Var "b"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "a")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set (Var "a"))  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set (Var "b")) ")" ) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6: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  "(" (Set (Var "a"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "b")) ")" )  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set  "(" (Set (Var "b"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "a")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6: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")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "b")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "c")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set (Var "a"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set (Var "b"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "c")) ")" ) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6:5 (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"::: ) ) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set (Var "b"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "c")) ")" ) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "b")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "c")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6:6 (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"::: ) ) "holds"  (Bool (Set (Set  "(" (Set (Var "c"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "a")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set  "(" (Set (Var "c"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "b")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set (Var "c"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "b")) ")" ) ")" ) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6: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")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "b")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "c")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "c")) ")" )  ($#k5_bvfunc_1 :::"'or'"::: )  (Set  "(" (Set (Var "b"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "c")) ")" ) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6: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")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "c")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set  "(" (Set (Var "b"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "c")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "b")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "c")) ")" ) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6: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")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "c")) ")" )  ($#k2_bvfunc_1 :::"'&'"::: )  (Set  "(" (Set (Var "b"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "c")) ")" ) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "b")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "c")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6: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 (Set (Set  "(" (Set (Var "a"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set (Var "b"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "b")) ")" ) ")" ) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "a")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6: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")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "b")) ")" )  ($#k2_bvfunc_1 :::"'&'"::: )  (Set  "(" (Set (Var "a"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "c")) ")" ) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set (Var "a"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set  "(" (Set (Var "b"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "c")) ")" ) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6: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")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set  "(" (Set (Var "b"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "c")) ")" ) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "b")) ")" )  ($#k5_bvfunc_1 :::"'or'"::: )  (Set  "(" (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "c")) ")" ) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6: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")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "c")) ")" )  ($#k2_bvfunc_1 :::"'&'"::: )  (Set  "(" (Set (Var "b"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "c")) ")" ) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "b")) ")" )  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "c")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6: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")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "b")) ")" )  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "c")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "c")) ")" )  ($#k5_bvfunc_1 :::"'or'"::: )  (Set  "(" (Set (Var "b"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "c")) ")" ) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6: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")) "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")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y"))))) "holds"  (Bool (Set (Set (Var "a"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "b")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6: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")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) )  "st" (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"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "c")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set (Var "b"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "c")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6:17 (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"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "b")))  ($#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")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set (Var "b"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "c")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6: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 "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) )  "st" (Bool (Bool (Set (Set (Var "c"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "a")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))) & (Bool (Set (Set (Var "c"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "b")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y"))))) "holds"  (Bool (Set (Set (Var "c"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "b")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6:19 (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"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "c")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))) & (Bool (Set (Set (Var "b"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "c")))  ($#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 "b")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "c")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6:20 (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"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "b")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))) & (Bool (Set   ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "a")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y"))))) "holds"  (Bool (Set (Var "b"))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6:21 (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"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "b")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))) & (Bool (Set (Set (Var "c"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (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")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set (Var "b"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "d")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6:22 (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"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "b")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))) & (Bool (Set (Set (Var "c"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (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")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (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_6: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"::: ) )  "st" (Bool (Bool (Set (Set  "(" (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "b")) ")" ) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "a")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y"))))) "holds"  (Bool (Set (Set (Var "a"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "b")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6: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"::: ) )  "st" (Bool (Bool (Set (Set (Var "a"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "b")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y"))))) "holds"  (Bool (Set (Set (Var "b"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "a")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6: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 "b")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) )  "st" (Bool (Bool (Set (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "a")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (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 "b")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "a")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6: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"::: ) ) "holds"  (Bool (Set (Set (Var "a"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set (Var "a"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "b")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6: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"::: ) ) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "b")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "a")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "b")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6:28 (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  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set  "(" (Set (Var "a"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "b")) ")" ) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "a")) ")" )  ($#k2_bvfunc_1 :::"'&'"::: )  (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "b")) ")" ) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6:29 (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  "(" (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "a")) ")" )  ($#k2_bvfunc_1 :::"'&'"::: )  (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "b")) ")" ) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set  "(" (Set (Var "a"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "b")) ")" ) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6:30 (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  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set  "(" (Set (Var "a"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "b")) ")" ) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "a")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6:31 (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  "(" (Set (Var "a"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "a")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "a")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6:32 (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  "(" (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "a")) ")" ) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "b")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6:33 (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  "(" (Set (Var "a"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "b")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "a")) ")" )  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "b")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6:34 (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  "(" (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "b")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set  "(" (Set (Var "a"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "b")) ")" ) ")" ) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6:35 (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  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set  "(" (Set (Var "a"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "b")) ")" ) ")" ) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "b")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6:36 (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  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set  "(" (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "b")) ")" ) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "a")) ")" )  ($#k5_bvfunc_1 :::"'or'"::: )  (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "b")) ")" ) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6:37 (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  "(" (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "a")) ")" )  ($#k5_bvfunc_1 :::"'or'"::: )  (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set (Var "b")) ")" ) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "("  ($#k1_bvfunc_1 :::"'not'"::: )  (Set  "(" (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "b")) ")" ) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6:38 (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  "(" (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "b")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "a")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6:39 (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  "(" (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "b")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set (Var "a"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "b")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6:40 (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  "(" (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "b")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "b")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6:41 (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"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "a")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6:42 (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  "(" (Set (Var "a"))  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set (Var "b")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set (Var "a"))  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set (Var "b")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6:43 (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  "(" (Set (Var "a"))  ($#k10_bvfunc_1 :::"'eqv'"::: )  (Set (Var "b")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (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_6:44 (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"::: ) ) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "b")) ")" )  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "c")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set (Var "a"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set  "(" (Set (Var "b"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "c")) ")" ) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6:45 (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"::: ) ) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "b")) ")" )  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "c")) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set (Var "a"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set  "(" (Set (Var "b"))  ($#k2_bvfunc_1 :::"'&'"::: )  (Set (Var "c")) ")" ) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BVFUNC_6:46 (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"::: ) ) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set  "(" (Set (Var "b"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "c")) ")" ) ")" )  ($#k9_bvfunc_1 :::"'imp'"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "b")) ")" )  ($#k5_bvfunc_1 :::"'or'"::: )  (Set (Var "c")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k12_bvfunc_1 :::"I_el"::: )  (Set (Var "Y")))))) ;