:: SHEFFER2  semantic presentation begin  definitionlet "L" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_sheffer1 :::"ShefferStr"::: )  ; attr "L" is  :::"satisfying_Sh_1":::  means :: SHEFFER2:def 1 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" "L" "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "y")))); end; 




:: deftheorem    defines :::"satisfying_Sh_1"::: SHEFFER2:def 1 :  (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_sheffer1 :::"ShefferStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "L")) "is"   ($#v1_sheffer2 :::"satisfying_Sh_1"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "y"))))  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v7_struct_0 :::"trivial"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )    for    ($#l1_sheffer1 :::"ShefferStr"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#v1_sheffer2 :::"satisfying_Sh_1"::: )    for    ($#l1_sheffer1 :::"ShefferStr"::: )  ; 
end; 



theorem :: SHEFFER2:1 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "u"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ))))) ; 
 
theorem :: SHEFFER2:2 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ))))) ; 
 
theorem :: SHEFFER2:3 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "y"))))) ; 
 
theorem :: SHEFFER2:4 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))))) ; 
 
theorem :: SHEFFER2:5 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")))))) ; 
 
theorem :: SHEFFER2:6 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))) ; 
 
theorem :: SHEFFER2:7 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))) ; 
 
theorem :: SHEFFER2:8 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")))))) ; 
 
theorem :: SHEFFER2:9 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ))))) ; 
 
theorem :: SHEFFER2:10 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")))))) ; 
 
theorem :: SHEFFER2:11 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))) ; 
 
theorem :: SHEFFER2:12 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")))))) ; 
 
theorem :: SHEFFER2:13 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")))))) ; 
 
theorem :: SHEFFER2:14 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")))))) ; 
 
theorem :: SHEFFER2:15 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))) ; 
 
theorem :: SHEFFER2:16 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))) ; 
 
theorem :: SHEFFER2:17 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")))))) ; 
 
theorem :: SHEFFER2:18 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ))))) ; 
 
theorem :: SHEFFER2:19 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")))))) ; 
 
theorem :: SHEFFER2:20 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")))))) ; 
 
theorem :: SHEFFER2:21 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))) ; 
 
theorem :: SHEFFER2:22 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "y"))))) ; 
 
theorem :: SHEFFER2:23 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))) ; 
 
theorem :: SHEFFER2:24 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "y"))))) ; 
 
theorem :: SHEFFER2:25 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))) ; 
 
theorem :: SHEFFER2:26 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")))))) ; 
 
theorem :: SHEFFER2:27 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ))))) ; 
 
theorem :: SHEFFER2:28 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ))))) ; 
 
theorem :: SHEFFER2:29 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "u"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))))) ; 
 
theorem :: SHEFFER2:30 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))))) ; 
 
theorem :: SHEFFER2:31 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "u"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))) ; 
 
theorem :: SHEFFER2:32 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")))))) ; 
 
theorem :: SHEFFER2:33 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ))))) ; 
 
theorem :: SHEFFER2:34 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")))))) ; 
 
theorem :: SHEFFER2:35 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:36 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")))))) ; 
 
theorem :: SHEFFER2:37 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))))) ; 
 
theorem :: SHEFFER2:38 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ))))) ; 
 
theorem :: SHEFFER2:39 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:40 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "u")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "u"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))))) ; 
 
theorem :: SHEFFER2:41 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ))))) ; 
 
theorem :: SHEFFER2:42 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ))))) ; 
 
theorem :: SHEFFER2:43 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))))) ; 
 
theorem :: SHEFFER2:44 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ))))) ; 
 
theorem :: SHEFFER2:45 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:46 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:47 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:48 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ))))) ; 
 
theorem :: SHEFFER2:49 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")))))) ; 
 
theorem :: SHEFFER2:50 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))))) ; 
 
theorem :: SHEFFER2:51 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ))))) ; 
 
theorem :: SHEFFER2:52 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "y"))))) ; 
 
theorem :: SHEFFER2:53 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ))))) ; 
 
theorem :: SHEFFER2:54 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ))))) ; 
 
theorem :: SHEFFER2:55 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:56 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "u"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ))))) ; 
 
theorem :: SHEFFER2:57 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:58 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")))))) ; 
 
theorem :: SHEFFER2:59 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")))))) ; 
 
theorem :: SHEFFER2:60 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:61 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:62 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ))))) ; 
 
theorem :: SHEFFER2:63 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:64 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:65 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:66 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:67 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_sheffer1 :::"ShefferStr"::: )    "st" (Bool (Bool (Set (Var "L")) "is"   ($#v1_sheffer2 :::"satisfying_Sh_1"::: )  )) "holds"  (Bool (Set (Var "L")) "is"   ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )  )) ; 
 
theorem :: SHEFFER2:68 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_sheffer1 :::"ShefferStr"::: )    "st" (Bool (Bool (Set (Var "L")) "is"   ($#v1_sheffer2 :::"satisfying_Sh_1"::: )  )) "holds"  (Bool (Set (Var "L")) "is"   ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )  )) ; 
 
theorem :: SHEFFER2:69 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_sheffer1 :::"ShefferStr"::: )    "st" (Bool (Bool (Set (Var "L")) "is"   ($#v1_sheffer2 :::"satisfying_Sh_1"::: )  )) "holds"  (Bool (Set (Var "L")) "is"   ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )  )) ; 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_lattices :::"Lattice-like"::: )     ($#v17_lattices :::"Boolean"::: )     ($#v8_robbins1 :::"well-complemented"::: )     ($#v10_robbins1 :::"de_Morgan"::: )     ($#v9_sheffer1 :::"properly_defined"::: )     ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#v1_sheffer2 :::"satisfying_Sh_1"::: )    for    ($#l3_sheffer1 :::"ShefferOrthoLattStr"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v9_sheffer1 :::"properly_defined"::: )     ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_lattices :::"Lattice-like"::: )     ($#v17_lattices :::"Boolean"::: )    for    ($#l3_sheffer1 :::"ShefferOrthoLattStr"::: )  ; 

cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_lattices :::"Lattice-like"::: )     ($#v17_lattices :::"Boolean"::: )     ($#v8_robbins1 :::"well-complemented"::: )     ($#v9_sheffer1 :::"properly_defined"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )    for    ($#l3_sheffer1 :::"ShefferOrthoLattStr"::: )  ; 
end; begin  












theorem :: SHEFFER2:70 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")))))) ; 
 
theorem :: SHEFFER2:71 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:72 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "y")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "w"))))) ; 
 
theorem :: SHEFFER2:73 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "q")) "," (Set (Var "p")) "," (Set (Var "y")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:74 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "q")) "," (Set (Var "p")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:75 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "w")) "," (Set (Var "p")) "," (Set (Var "y")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:76 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))))) ; 
 
theorem :: SHEFFER2:77 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "y")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "w"))))) ; 
 
theorem :: SHEFFER2:78 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "y")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "w"))))) ; 
 
theorem :: SHEFFER2:79 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "y")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "w"))))) ; 
 
theorem :: SHEFFER2:80 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")))))) ; 
 
theorem :: SHEFFER2:81 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")))))) ; 
 
theorem :: SHEFFER2:82 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "y")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")))))) ; 
 
theorem :: SHEFFER2:83 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "y")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")))))) ; 
 
theorem :: SHEFFER2:84 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))))) ; 
 
theorem :: SHEFFER2:85 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))))) ; 
 
theorem :: SHEFFER2:86 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))))) ; 
 
theorem :: SHEFFER2:87 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))))) ; 
 
theorem :: SHEFFER2:88 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "y")) "," (Set (Var "q")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:89 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "q")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:90 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "q")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))))) ; 
 
theorem :: SHEFFER2:91 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))))) ; 
 
theorem :: SHEFFER2:92 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))))) ; 
 
theorem :: SHEFFER2:93 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "z")) "," (Set (Var "w")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:94 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "z")) "," (Set (Var "w")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ))))) ; 
 
theorem :: SHEFFER2:95 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "w")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))))) ; 
 
theorem :: SHEFFER2:96 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))))) ; 
 
theorem :: SHEFFER2:97 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))))) ; 
 
theorem :: SHEFFER2:98 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "z")) "," (Set (Var "q")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:99 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "q")) "," (Set (Var "z")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:100 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "q")) "," (Set (Var "z")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:101 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "w")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")))))) ; 
 
theorem :: SHEFFER2:102 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "w")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "p"))))) ; 
 
theorem :: SHEFFER2:103 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "y")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")))))) ; 
 
theorem :: SHEFFER2:104 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "y")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")))))) ; 
 
theorem :: SHEFFER2:105 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "p"))))) ; 
 
theorem :: SHEFFER2:106 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "w")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "p"))))) ; 
 
theorem :: SHEFFER2:107 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "w"))))) ; 
 
theorem :: SHEFFER2:108 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")))))) ; 
 
theorem :: SHEFFER2:109 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "w"))))) ; 
 
theorem :: SHEFFER2:110 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "w")) "," (Set (Var "q")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:111 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "q")) "," (Set (Var "w")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:112 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "w"))))) ; 
 
theorem :: SHEFFER2:113 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "w"))))) ; 
 
theorem :: SHEFFER2:114 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "q")) "," (Set (Var "p")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:115 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "q")) "," (Set (Var "z")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:116 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "q")) "," (Set (Var "z")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:117 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "w")) "," (Set (Var "q")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:118 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "q")) "," (Set (Var "p")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")))))) ; 
 
theorem :: SHEFFER2:119 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")))))) ; 
 
theorem :: SHEFFER2:120 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))))) ; 
 
theorem :: SHEFFER2:121 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))))) ; 
 
theorem :: SHEFFER2:122 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))))) ; 
 
theorem :: SHEFFER2:123 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")))))) ; 
 
theorem :: SHEFFER2:124 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))) ; 
 
theorem :: SHEFFER2:125 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))))) ; 
 
theorem :: SHEFFER2:126 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")))))) ; 
 
theorem :: SHEFFER2:127 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "z")) "," (Set (Var "y")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ))))) ; 
 
theorem :: SHEFFER2:128 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "z")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "y"))))) ; 
 
theorem :: SHEFFER2:129 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")))))) ; 
 
theorem :: SHEFFER2:130 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:131 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "y")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")))))) ; 
 
theorem :: SHEFFER2:132 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "w"))))) ; 
 
theorem :: SHEFFER2:133 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "w")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "w"))))) ; 
 
theorem :: SHEFFER2:134 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "y")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "w"))))) ; 
 
theorem :: SHEFFER2:135 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "w"))))) ; 
 
theorem :: SHEFFER2:136 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "y")) "," (Set (Var "p")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "w"))))) ; 
 
theorem :: SHEFFER2:137 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:138 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "q")) "," (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:139 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "q")) "," (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ))))) ; 
 
theorem :: SHEFFER2:140 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "z")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "y")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:141 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "z")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "y")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:142 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "z")) "," (Set (Var "q")) "," (Set (Var "y")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:143 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "v")) "," (Set (Var "p")) "," (Set (Var "y")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "v")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "v"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")))))) ; 
 
theorem :: SHEFFER2:144 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "z")) "," (Set (Var "v")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "v")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "v"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "v")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "v")) ")" ))))) ; 
 
theorem :: SHEFFER2:145 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ))))) ; 
 
theorem :: SHEFFER2:146 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "z")) "," (Set (Var "y")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ))))) ; 
 
theorem :: SHEFFER2:147 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ))))) ; 
 
theorem :: SHEFFER2:148 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "z")) "," (Set (Var "w")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ))))) ; 
 
theorem :: SHEFFER2:149 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "z")) "," (Set (Var "y")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:150 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "z")) "," (Set (Var "y")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:151 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "z")) "," (Set (Var "p")) "," (Set (Var "y")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" ) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:152 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "z")) "," (Set (Var "p")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))))) ; 
 
theorem :: SHEFFER2:153 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "w")) "," (Set (Var "q")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" ))))) ; 
 
theorem :: SHEFFER2:154 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "w")) "," (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" ))))) ; 
 
theorem :: SHEFFER2:155 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "z")) "," (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" ) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:156 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "w")) "," (Set (Var "z")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "w"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "w")) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:157 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "q")) "," (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:158 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "q")) "," (Set (Var "z")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" ) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:159 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "z")) "," (Set (Var "x")) "," (Set (Var "q")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "z"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "z")) ")" ) ")" ) ")" ) ")" ))))) ; 
 
theorem :: SHEFFER2:160 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "q")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "y")) ")" )  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "x"))  ($#k5_sheffer1 :::"|"::: )  (Set  "(" (Set (Var "y"))  ($#k5_sheffer1 :::"|"::: )  (Set (Var "q")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))) ; 
 
theorem :: SHEFFER2:161 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )     ($#l1_sheffer1 :::"ShefferStr"::: )   "holds"  (Bool (Set (Var "L")) "is"   ($#v1_sheffer2 :::"satisfying_Sh_1"::: )  )) ; 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )    for    ($#l1_sheffer1 :::"ShefferStr"::: )  ; 

cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: )     ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: )     ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: )    for    ($#l1_sheffer1 :::"ShefferStr"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v9_sheffer1 :::"properly_defined"::: )     ($#v1_sheffer2 :::"satisfying_Sh_1"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_lattices :::"Lattice-like"::: )     ($#v17_lattices :::"Boolean"::: )    for    ($#l3_sheffer1 :::"ShefferOrthoLattStr"::: )  ; 

cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_lattices :::"Lattice-like"::: )     ($#v17_lattices :::"Boolean"::: )     ($#v8_robbins1 :::"well-complemented"::: )     ($#v9_sheffer1 :::"properly_defined"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_sheffer2 :::"satisfying_Sh_1"::: )    for    ($#l3_sheffer1 :::"ShefferOrthoLattStr"::: )  ; 
end;