:: REALSET3  semantic presentation begin  
theorem :: REALSET3:1 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::) "holds"  (Bool (Set (Set  "("  ($#k5_realset2 :::"revf"::: )  (Set (Var "F")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k5_struct_0 :::"1."::: )  (Set (Var "F")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "F"))))) ; 
 
theorem :: REALSET3:2 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set (Var "F"))) "holds"  (Bool (Set (Set  "("  ($#k5_realset2 :::"revf"::: )  (Set (Var "F")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set  "(" (Set  "("  ($#k5_realset2 :::"revf"::: )  (Set (Var "F")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "b")) ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "b")) "," (Set  "(" (Set  "("  ($#k5_realset2 :::"revf"::: )  (Set (Var "F")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "a")) ")" ) ")" )))) ; 
 
theorem :: REALSET3:3 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set (Var "F"))) "holds"  (Bool (Set (Set  "("  ($#k5_realset2 :::"revf"::: )  (Set (Var "F")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set  "(" (Set  "("  ($#k5_realset2 :::"revf"::: )  (Set (Var "F")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "a")) ")" ) "," (Set  "(" (Set  "("  ($#k5_realset2 :::"revf"::: )  (Set (Var "F")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "b")) ")" ) ")" )))) ; 
 
theorem :: REALSET3:4 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds"   (Bool  "("  (Bool (Set (Set (Var "a"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "d")))) "iff" (Bool (Set (Set (Var "a"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "c"))))  ")" ))) ; 
 
theorem :: REALSET3:5 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "d")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set (Var "F"))) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set  "(" (Set  "("  ($#k5_realset2 :::"revf"::: )  (Set (Var "F")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "b")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "c")) "," (Set  "(" (Set  "("  ($#k5_realset2 :::"revf"::: )  (Set (Var "F")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "d")) ")" ) ")" )) "iff" (Bool (Set (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "d")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "b")) "," (Set (Var "c")) ")" ))  ")" )))) ; 
 
theorem :: REALSET3:6 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "c")) "," (Set (Var "d")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set (Var "F"))) "holds"  (Bool (Set (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set  "(" (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set  "(" (Set  "("  ($#k5_realset2 :::"revf"::: )  (Set (Var "F")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "c")) ")" ) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "b")) "," (Set  "(" (Set  "("  ($#k5_realset2 :::"revf"::: )  (Set (Var "F")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "d")) ")" ) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set  "(" (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k5_realset2 :::"revf"::: )  (Set (Var "F")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "c")) "," (Set (Var "d")) ")"  ")" ) ")" ) ")" ))))) ; 
 
theorem :: REALSET3:7 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "c")) "," (Set (Var "d")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set (Var "F"))) "holds"  (Bool (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "F")))  ($#k1_binop_1 :::"."::: )   "(" (Set  "(" (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set  "(" (Set  "("  ($#k5_realset2 :::"revf"::: )  (Set (Var "F")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "c")) ")" ) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "b")) "," (Set  "(" (Set  "("  ($#k5_realset2 :::"revf"::: )  (Set (Var "F")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "d")) ")" ) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set  "(" (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "F")))  ($#k5_binop_1 :::"."::: )   "(" (Set  "(" (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "d")) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "b")) "," (Set (Var "c")) ")"  ")" ) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k5_realset2 :::"revf"::: )  (Set (Var "F")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "c")) "," (Set (Var "d")) ")"  ")" ) ")" ) ")" ))))) ; 
 definitionlet "F" be   ($#l6_algstr_0 :::"Field":::); func  :::"osf"::: "F" ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "F") means :: REALSET3:def 1 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" "F" "holds"  (Bool (Set it  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" "F")  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set  "(" (Set  "("  ($#k5_vectsp_1 :::"comp"::: )  "F" ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "y")) ")" ) ")" ))); end; 





:: deftheorem    defines :::"osf"::: REALSET3:def 1 :  (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F"))) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_realset3 :::"osf"::: )  (Set (Var "F")))) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds"  (Bool (Set (Set (Var "b2"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "F")))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set  "(" (Set  "("  ($#k5_vectsp_1 :::"comp"::: )  (Set (Var "F")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "y")) ")" ) ")" )))  ")" ))); 
 
theorem :: REALSET3:8 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds"  (Bool (Set (Set  "("  ($#k1_realset3 :::"osf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "F")))))) ; 
 
theorem :: REALSET3:9 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds"  (Bool (Set (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set  "(" (Set  "("  ($#k1_realset3 :::"osf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "b")) "," (Set (Var "c")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_realset3 :::"osf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set  "(" (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "c")) ")"  ")" ) ")" )))) ; 
 
theorem :: REALSET3:10 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds"  (Bool (Set (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set  "(" (Set  "("  ($#k1_realset3 :::"osf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set (Var "c")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_realset3 :::"osf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set  "(" (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "c")) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "b")) "," (Set (Var "c")) ")"  ")" ) ")" )))) ; 
 
theorem :: REALSET3:11 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds"  (Bool (Set (Set  "("  ($#k1_realset3 :::"osf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_vectsp_1 :::"comp"::: )  (Set (Var "F")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  "("  ($#k1_realset3 :::"osf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "b")) "," (Set (Var "a")) ")"  ")" ))))) ; 
 
theorem :: REALSET3:12 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds"  (Bool (Set (Set  "("  ($#k1_realset3 :::"osf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set  "(" (Set  "("  ($#k5_vectsp_1 :::"comp"::: )  (Set (Var "F")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "a")) ")" ) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_vectsp_1 :::"comp"::: )  (Set (Var "F")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "F")))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ))))) ; 
 
theorem :: REALSET3:13 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k1_realset3 :::"osf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_realset3 :::"osf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "c")) "," (Set (Var "d")) ")" )) "iff" (Bool (Set (Set (Var "a"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "c"))))  ")" ))) ; 
 
theorem :: REALSET3:14 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds"  (Bool (Set (Set  "("  ($#k1_realset3 :::"osf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "F")) ")" ) "," (Set (Var "a")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_vectsp_1 :::"comp"::: )  (Set (Var "F")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))))) ; 
 
theorem :: REALSET3:15 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds"  (Bool (Set (Set  "("  ($#k1_realset3 :::"osf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "F")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "a"))))) ; 
 
theorem :: REALSET3:16 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds"   (Bool  "("  (Bool (Set (Set (Var "a"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "c"))) "iff" (Bool (Set (Set  "("  ($#k1_realset3 :::"osf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "c")) "," (Set (Var "a")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" ))) ; 
 
theorem :: REALSET3:17 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds"   (Bool  "("  (Bool (Set (Set (Var "a"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "c"))) "iff" (Bool (Set (Set  "("  ($#k1_realset3 :::"osf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "c")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ))) ; 
 
theorem :: REALSET3:18 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds"  (Bool (Set (Set  "("  ($#k1_realset3 :::"osf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set  "(" (Set  "("  ($#k1_realset3 :::"osf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "b")) "," (Set (Var "c")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "F")))  ($#k5_binop_1 :::"."::: )   "(" (Set  "(" (Set  "("  ($#k1_realset3 :::"osf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set (Var "c")) ")" )))) ; 
 
theorem :: REALSET3:19 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds"  (Bool (Set (Set  "("  ($#k1_realset3 :::"osf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set  "(" (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "F")))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "b")) "," (Set (Var "c")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_realset3 :::"osf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set  "(" (Set  "("  ($#k1_realset3 :::"osf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set (Var "c")) ")" )))) ; 
 definitionlet "F" be   ($#l6_algstr_0 :::"Field":::); func  :::"ovf"::: "F" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "F") "," (Set  "("  ($#k8_struct_0 :::"NonZero"::: )  "F" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "F") means :: REALSET3:def 2 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" "F"  (Bool  "for" (Set (Var "y")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_struct_0 :::"NonZero"::: )  "F") "holds"  (Bool (Set it  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_realset2 :::"omf"::: )  "F" ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set  "(" (Set  "("  ($#k5_realset2 :::"revf"::: )  "F" ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "y")) ")" ) ")" )))); end; 





:: deftheorem    defines :::"ovf"::: REALSET3:def 2 :  (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F"))) "," (Set  "("  ($#k8_struct_0 :::"NonZero"::: )  (Set (Var "F")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F"))) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_realset3 :::"ovf"::: )  (Set (Var "F")))) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "y")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set (Var "F"))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set  "(" (Set  "("  ($#k5_realset2 :::"revf"::: )  (Set (Var "F")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "y")) ")" ) ")" ))))  ")" ))); 
 
theorem :: REALSET3:20 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set (Var "F"))) "holds"  (Bool (Set (Set  "("  ($#k2_realset3 :::"ovf"::: )  (Set (Var "F")) ")" )  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "F")))))) ; 
 
theorem :: REALSET3:21 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "c")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set (Var "F"))) "holds"  (Bool (Set (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set  "(" (Set  "("  ($#k2_realset3 :::"ovf"::: )  (Set (Var "F")) ")" )  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "b")) "," (Set (Var "c")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_realset3 :::"ovf"::: )  (Set (Var "F")) ")" )  ($#k2_binop_1 :::"."::: )   "(" (Set  "(" (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set (Var "c")) ")" ))))) ; 
 
theorem :: REALSET3:22 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set (Var "F"))) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set  "(" (Set  "("  ($#k2_realset3 :::"ovf"::: )  (Set (Var "F")) ")" )  ($#k2_binop_1 :::"."::: )   "(" (Set  "("  ($#k5_struct_0 :::"1."::: )  (Set (Var "F")) ")" ) "," (Set (Var "a")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "F")))) & (Bool (Set (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set  "(" (Set  "("  ($#k2_realset3 :::"ovf"::: )  (Set (Var "F")) ")" )  ($#k2_binop_1 :::"."::: )   "(" (Set  "("  ($#k5_struct_0 :::"1."::: )  (Set (Var "F")) ")" ) "," (Set (Var "a")) ")"  ")" ) "," (Set (Var "a")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "F"))))  ")" ))) ; 
 
theorem :: REALSET3:23 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set (Var "F"))) "holds"  (Bool (Set (Set  "("  ($#k2_realset3 :::"ovf"::: )  (Set (Var "F")) ")" )  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_realset2 :::"revf"::: )  (Set (Var "F")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "("  ($#k2_realset3 :::"ovf"::: )  (Set (Var "F")) ")" )  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "b")) "," (Set (Var "a")) ")"  ")" ))))) ; 
 
theorem :: REALSET3:24 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set (Var "F"))) "holds"  (Bool (Set (Set  "("  ($#k2_realset3 :::"ovf"::: )  (Set (Var "F")) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set  "(" (Set  "("  ($#k5_realset2 :::"revf"::: )  (Set (Var "F")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "a")) ")" ) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_realset2 :::"revf"::: )  (Set (Var "F")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ))))) ; 
 
theorem :: REALSET3:25 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "d")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set (Var "F"))) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k2_realset3 :::"ovf"::: )  (Set (Var "F")) ")" )  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_realset3 :::"ovf"::: )  (Set (Var "F")) ")" )  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "c")) "," (Set (Var "d")) ")" )) "iff" (Bool (Set (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "d")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "b")) "," (Set (Var "c")) ")" ))  ")" )))) ; 
 
theorem :: REALSET3:26 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set (Var "F"))) "holds"  (Bool (Set (Set  "("  ($#k2_realset3 :::"ovf"::: )  (Set (Var "F")) ")" )  ($#k2_binop_1 :::"."::: )   "(" (Set  "("  ($#k5_struct_0 :::"1."::: )  (Set (Var "F")) ")" ) "," (Set (Var "a")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_realset2 :::"revf"::: )  (Set (Var "F")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))))) ; 
 
theorem :: REALSET3:27 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds"  (Bool (Set (Set  "("  ($#k2_realset3 :::"ovf"::: )  (Set (Var "F")) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set  "("  ($#k5_struct_0 :::"1."::: )  (Set (Var "F")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "a"))))) ; 
 
theorem :: REALSET3:28 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set (Var "F")))  (Bool  "for" (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "c"))) "iff" (Bool (Set (Set  "("  ($#k2_realset3 :::"ovf"::: )  (Set (Var "F")) ")" )  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "c")) "," (Set (Var "a")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" )))) ; 
 
theorem :: REALSET3:29 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "b")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set (Var "F"))) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "c"))) "iff" (Bool (Set (Set  "("  ($#k2_realset3 :::"ovf"::: )  (Set (Var "F")) ")" )  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "c")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" )))) ; 
 
theorem :: REALSET3:30 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set (Var "F"))) "holds"  (Bool (Set (Set  "("  ($#k2_realset3 :::"ovf"::: )  (Set (Var "F")) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set  "(" (Set  "("  ($#k2_realset3 :::"ovf"::: )  (Set (Var "F")) ")" )  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "b")) "," (Set (Var "c")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set  "(" (Set  "("  ($#k2_realset3 :::"ovf"::: )  (Set (Var "F")) ")" )  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set (Var "c")) ")" ))))) ; 
 
theorem :: REALSET3:31 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set (Var "F"))) "holds"  (Bool (Set (Set  "("  ($#k2_realset3 :::"ovf"::: )  (Set (Var "F")) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set  "(" (Set  "("  ($#k4_realset2 :::"omf"::: )  (Set (Var "F")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "b")) "," (Set (Var "c")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_realset3 :::"ovf"::: )  (Set (Var "F")) ")" )  ($#k2_binop_1 :::"."::: )   "(" (Set  "(" (Set  "("  ($#k2_realset3 :::"ovf"::: )  (Set (Var "F")) ")" )  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set (Var "c")) ")" ))))) ;