:: ORTSP_1 semantic presentation begin definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_symsp_1 :::"SymStr"::: ) "over" (Set (Const "F")); attr "IT" is :::"OrtSp-like"::: means :: ORTSP_1:def 1 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element":::) "of" "F" "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) "IT")) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) "IT")) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) "IT")) & (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) "IT"))) "implies" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "(" (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Bool "not" (Set (Var "b")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Bool "not" (Set (Var "c")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Bool "not" (Set (Var "d")) ($#r1_orders_2 :::"_|_"::: ) )) ")" )) ")" & "(" (Bool (Bool (Set (Var "b")) ($#r1_orders_2 :::"_|_"::: ) )) "implies" (Bool (Set (Var "b")) ($#r1_orders_2 :::"_|_"::: ) ) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) ) & (Bool (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) "implies" (Bool (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) ))) "implies" (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element":::) "of" "F" "st" (Bool (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) ")" & "(" (Bool (Bool (Set (Set (Var "b")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "c"))) ($#r1_orders_2 :::"_|_"::: ) ) & (Bool (Set (Set (Var "c")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "a"))) ($#r1_orders_2 :::"_|_"::: ) )) "implies" (Bool (Set (Set (Var "a")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "b"))) ($#r1_orders_2 :::"_|_"::: ) ) ")" ")" ))); end; :: deftheorem defines :::"OrtSp-like"::: ORTSP_1:def 1 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_symsp_1 :::"SymStr"::: ) "over" (Set (Var "F")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_ortsp_1 :::"OrtSp-like"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "IT")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "IT")))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "IT")))) & (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "IT"))))) "implies" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Bool "not" (Set (Var "b")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Bool "not" (Set (Var "c")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Bool "not" (Set (Var "d")) ($#r1_orders_2 :::"_|_"::: ) )) ")" )) ")" & "(" (Bool (Bool (Set (Var "b")) ($#r1_orders_2 :::"_|_"::: ) )) "implies" (Bool (Set (Var "b")) ($#r1_orders_2 :::"_|_"::: ) ) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) ) & (Bool (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) "implies" (Bool (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) ))) "implies" (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "st" (Bool (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) ")" & "(" (Bool (Bool (Set (Set (Var "b")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "c"))) ($#r1_orders_2 :::"_|_"::: ) ) & (Bool (Set (Set (Var "c")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "a"))) ($#r1_orders_2 :::"_|_"::: ) )) "implies" (Bool (Set (Set (Var "a")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "b"))) ($#r1_orders_2 :::"_|_"::: ) ) ")" ")" ))) ")" ))); registrationlet "F" be ($#l6_algstr_0 :::"Field":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v1_symsp_1 :::"strict"::: ) ($#v1_ortsp_1 :::"OrtSp-like"::: ) for ($#l1_symsp_1 :::"SymStr"::: ) "over" "F"; end; definitionlet "F" be ($#l6_algstr_0 :::"Field":::); mode OrtSp of "F" is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v1_ortsp_1 :::"OrtSp-like"::: ) ($#l1_symsp_1 :::"SymStr"::: ) "over" "F"; end; theorem :: ORTSP_1:1 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )))) ; theorem :: ORTSP_1:2 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "b")) ($#r1_orders_2 :::"_|_"::: ) )) "holds" (Bool (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )))) ; theorem :: ORTSP_1:3 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "b")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Set (Var "b")) ($#r1_orders_2 :::"_|_"::: ) )) "holds" (Bool "not" (Bool (Set (Var "b")) ($#r1_orders_2 :::"_|_"::: ) ))))) ; theorem :: ORTSP_1:4 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) "holds" (Bool "not" (Bool (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) ))))) ; theorem :: ORTSP_1:5 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Bool "not" (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))))) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Bool "not" (Set (Set (Var "l")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "a"))) ($#r1_orders_2 :::"_|_"::: ) )) ")" ))))) ; theorem :: ORTSP_1:6 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "b")) ($#r1_orders_2 :::"_|_"::: ) )) "holds" (Bool (Set (Var "b")) ($#r1_orders_2 :::"_|_"::: ) )))) ; theorem :: ORTSP_1:7 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "d")) ($#r1_orders_2 :::"_|_"::: ) ) & (Bool (Set (Var "d")) ($#r1_orders_2 :::"_|_"::: ) )) "holds" (Bool (Set (Var "d")) ($#r1_orders_2 :::"_|_"::: ) )))) ; theorem :: ORTSP_1:8 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) ) & (Bool (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) "holds" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Var "l"))))))) ; theorem :: ORTSP_1:9 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) ) & (Bool (Set (Var "b")) ($#r1_orders_2 :::"_|_"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "b"))) ($#r1_orders_2 :::"_|_"::: ) )))) ; theorem :: ORTSP_1:10 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "F")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))) & (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "S")))))) "holds" (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool "not" (Set (Var "b")) ($#r1_orders_2 :::"_|_"::: ) ))))) ; definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "S" be ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Const "F")); let "a", "b", "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); assume (Bool (Bool "not" (Set (Const "a")) ($#r1_orders_2 :::"_|_"::: ) )) ; func :::"ProJ"::: "(" "a" "," "b" "," "x" ")" -> ($#m1_subset_1 :::"Element":::) "of" "F" means :: ORTSP_1:def 2 (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element":::) "of" "F" "st" (Bool (Bool "a" ($#r1_orders_2 :::"_|_"::: ) )) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Var "l")))); end; :: deftheorem defines :::"ProJ"::: ORTSP_1:def 2 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) ))) "holds" (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) ")" )) "iff" (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) "holds" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Var "l")))) ")" ))))); theorem :: ORTSP_1:11 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) ))) "holds" (Bool (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )))) ; theorem :: ORTSP_1:12 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) ))) "holds" (Bool (Set ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "l")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "l")) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) ")" ")" ))))))) ; theorem :: ORTSP_1:13 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) ))) "holds" (Bool (Set ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "y")) ")" ")" )))))) ; theorem :: ORTSP_1:14 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Set (Var "l")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F"))))) "holds" (Bool (Set ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "l")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "b")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "l")) ($#k11_algstr_0 :::"""::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) ")" ")" ))))))) ; theorem :: ORTSP_1:15 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Set (Var "l")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F"))))) "holds" (Bool (Set ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set "(" (Set (Var "l")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "a")) ")" ) "," (Set (Var "b")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) ")" )))))) ; theorem :: ORTSP_1:16 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) "holds" (Bool "(" (Bool (Set ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "b")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p")) ")" ) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )) & (Bool (Set ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "c")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )) ")" )))) ; theorem :: ORTSP_1:17 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Set (Var "b")) ($#r1_orders_2 :::"_|_"::: ) ) & (Bool (Set (Var "c")) ($#r1_orders_2 :::"_|_"::: ) )) "holds" (Bool (Set ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set "(" (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p")) ")" ) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ))))) ; theorem :: ORTSP_1:18 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) "holds" (Bool (Set ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "F"))))))) ; theorem :: ORTSP_1:19 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) ))) "holds" (Bool (Set ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "F"))))))) ; theorem :: ORTSP_1:20 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) ) "iff" (Bool (Set ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))) ")" )))) ; theorem :: ORTSP_1:21 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) ))) "holds" (Bool (Set (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "q")) ")" ")" ) ($#k11_algstr_0 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "q")) "," (Set (Var "p")) ")" ))))) ; theorem :: ORTSP_1:22 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) ))) "holds" (Bool (Set ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) ")" ")" ) ($#k11_algstr_0 :::"""::: ) ))))) ; theorem :: ORTSP_1:23 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Set (Set (Var "c")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a"))) ($#r1_orders_2 :::"_|_"::: ) )) "holds" (Bool (Set ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a")) ")" ")" )))))) ; theorem :: ORTSP_1:24 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "b")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Bool "not" (Set (Var "b")) ($#r1_orders_2 :::"_|_"::: ) ))) "holds" (Bool (Set ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) ")" ")" ) ($#k11_algstr_0 :::"""::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" )))))) ; theorem :: ORTSP_1:25 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Bool "not" (Set (Var "x")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Bool "not" (Set (Var "x")) ($#r1_orders_2 :::"_|_"::: ) ))) "holds" (Bool (Set (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "q")) "," (Set (Var "p")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "x")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "x")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) "," (Set (Var "p")) ")" ")" )))))) ; theorem :: ORTSP_1:26 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "q")) "," (Set (Var "b")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Bool "not" (Set (Var "x")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Bool "not" (Set (Var "x")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "x")) ")" ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "q")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "x")) ")" ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) "," (Set (Var "y")) ")" ")" )))))) ; theorem :: ORTSP_1:27 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "p")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Bool "not" (Set (Var "p")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Bool "not" (Set (Var "p")) ($#r1_orders_2 :::"_|_"::: ) ))) "holds" (Bool (Set (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "x")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "y")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "y")) "," (Set (Var "p")) "," (Set (Var "x")) ")" ")" )))))) ; definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "S" be ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Const "F")); let "x", "y", "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); assume (Bool (Bool "not" (Set (Const "a")) ($#r1_orders_2 :::"_|_"::: ) )) ; func :::"PProJ"::: "(" "a" "," "b" "," "x" "," "y" ")" -> ($#m1_subset_1 :::"Element":::) "of" "F" means :: ORTSP_1:def 3 (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" "S" "st" (Bool (Bool (Bool "not" "a" ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Bool "not" "x" ($#r1_orders_2 :::"_|_"::: ) ))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" "a" "," "b" "," (Set (Var "q")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "q")) "," "a" "," "x" ")" ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" "x" "," (Set (Var "q")) "," "y" ")" ")" )))) if (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" "S" "st" (Bool "(" (Bool (Bool "not" "a" ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Bool "not" "x" ($#r1_orders_2 :::"_|_"::: ) )) ")" )) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "F")); end; :: deftheorem defines :::"PProJ"::: ORTSP_1:def 3 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) ))) "holds" (Bool "for" (Set (Var "b7")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds" (Bool "(" "(" (Bool (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Bool "not" (Set (Var "x")) ($#r1_orders_2 :::"_|_"::: ) )) ")" ))) "implies" (Bool "(" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set ($#k2_ortsp_1 :::"PProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Bool "not" (Set (Var "x")) ($#r1_orders_2 :::"_|_"::: ) ))) "holds" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "q")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "x")) ")" ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k1_ortsp_1 :::"ProJ"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) "," (Set (Var "y")) ")" ")" )))) ")" ) ")" & "(" (Bool (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) ) "or" (Bool (Set (Var "x")) ($#r1_orders_2 :::"_|_"::: ) ) ")" ) ")" )) "implies" (Bool "(" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set ($#k2_ortsp_1 :::"PProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))) ")" ) ")" ")" ))))); theorem :: ORTSP_1:28 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) )) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "S"))))) "holds" (Bool (Set ($#k2_ortsp_1 :::"PProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F"))))))) ; theorem :: ORTSP_1:29 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k2_ortsp_1 :::"PProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))) "iff" (Bool (Set (Var "x")) ($#r1_orders_2 :::"_|_"::: ) ) ")" )))) ; theorem :: ORTSP_1:30 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) ))) "holds" (Bool (Set ($#k2_ortsp_1 :::"PProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_ortsp_1 :::"PProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "y")) "," (Set (Var "x")) ")" ))))) ; theorem :: ORTSP_1:31 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) ))) "holds" (Bool (Set ($#k2_ortsp_1 :::"PProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set "(" (Set (Var "l")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "y")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "l")) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k2_ortsp_1 :::"PProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ))))))) ; theorem :: ORTSP_1:32 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "S")) "being" ($#l1_symsp_1 :::"OrtSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"_|_"::: ) ))) "holds" (Bool (Set ($#k2_ortsp_1 :::"PProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set "(" (Set (Var "y")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_ortsp_1 :::"PProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k2_ortsp_1 :::"PProJ"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "z")) ")" ")" )))))) ;