:: DIRORT semantic presentation begin notationlet "AS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) ; let "a", "b", "c", "d" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AS")); synonym "a" "," "b" :::"'//'"::: "c" "," "d" for "a" "," "b" :::"//"::: "c" "," "d"; end; theorem :: DIRORT:1 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_analort :::"CESpace"::: ) "(" (Set (Var "V")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "u")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v")) "," (Set (Var "w"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "w")) "," (Set (Var "w"))) & "(" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "v1"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v1")) "," (Set (Var "u1"))) & (Bool (Bool "not" (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "v"))))) "implies" (Bool (Set (Var "u1")) ($#r1_hidden :::"="::: ) (Set (Var "v1"))) ")" & "(" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "v1"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "w"))) & (Bool (Bool "not" (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v1")) "," (Set (Var "w"))))) "implies" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "w")) "," (Set (Var "v1"))) ")" & "(" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "v1")))) "implies" (Bool (Set (Var "v")) "," (Set (Var "u")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v1")) "," (Set (Var "u1"))) ")" & "(" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "v1"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v1")) "," (Set (Var "w")))) "implies" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "w"))) ")" & (Bool "(" "not" (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v")) "," (Set (Var "v1"))) "or" (Bool (Set (Var "v")) "," (Set (Var "v1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u")) "," (Set (Var "u1"))) "or" (Bool (Set (Var "v")) "," (Set (Var "v1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "u"))) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_analort :::"CESpace"::: ) "(" (Set (Var "V")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) (Bool "ex" (Set (Var "u1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_analort :::"CESpace"::: ) "(" (Set (Var "V")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_hidden :::"<>"::: ) (Set (Var "u1"))) & (Bool (Set (Var "w")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u")) "," (Set (Var "v"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_analort :::"CESpace"::: ) "(" (Set (Var "V")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) (Bool "ex" (Set (Var "u1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_analort :::"CESpace"::: ) "(" (Set (Var "V")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_hidden :::"<>"::: ) (Set (Var "u1"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "w")) "," (Set (Var "u1"))) ")" )) ")" ) ")" ))) ; theorem :: DIRORT:2 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k6_analort :::"CMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "u")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v")) "," (Set (Var "w"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "w")) "," (Set (Var "w"))) & "(" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "v1"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v1")) "," (Set (Var "u1"))) & (Bool (Bool "not" (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "v"))))) "implies" (Bool (Set (Var "u1")) ($#r1_hidden :::"="::: ) (Set (Var "v1"))) ")" & "(" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "v1"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "w"))) & (Bool (Bool "not" (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v1")) "," (Set (Var "w"))))) "implies" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "w")) "," (Set (Var "v1"))) ")" & "(" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "v1")))) "implies" (Bool (Set (Var "v")) "," (Set (Var "u")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v1")) "," (Set (Var "u1"))) ")" & "(" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "v1"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v1")) "," (Set (Var "w")))) "implies" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "w"))) ")" & (Bool "(" "not" (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v")) "," (Set (Var "v1"))) "or" (Bool (Set (Var "v")) "," (Set (Var "v1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u")) "," (Set (Var "u1"))) "or" (Bool (Set (Var "v")) "," (Set (Var "v1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "u"))) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k6_analort :::"CMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) (Bool "ex" (Set (Var "u1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k6_analort :::"CMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_hidden :::"<>"::: ) (Set (Var "u1"))) & (Bool (Set (Var "w")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u")) "," (Set (Var "v"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k6_analort :::"CMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) (Bool "ex" (Set (Var "u1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k6_analort :::"CMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_hidden :::"<>"::: ) (Set (Var "u1"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "w")) "," (Set (Var "u1"))) ")" )) ")" ) ")" ))) ; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) ; attr "IT" is :::"Oriented_Orthogonality_Space-like"::: means :: DIRORT:def 1 (Bool "(" (Bool "(" "for" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "u")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v")) "," (Set (Var "w"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "w")) "," (Set (Var "w"))) & "(" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "v1"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v1")) "," (Set (Var "u1"))) & (Bool (Bool "not" (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "v"))))) "implies" (Bool (Set (Var "u1")) ($#r1_hidden :::"="::: ) (Set (Var "v1"))) ")" & "(" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "v1"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "w"))) & (Bool (Bool "not" (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v1")) "," (Set (Var "w"))))) "implies" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "w")) "," (Set (Var "v1"))) ")" & "(" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "v1")))) "implies" (Bool (Set (Var "v")) "," (Set (Var "u")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v1")) "," (Set (Var "u1"))) ")" & "(" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "v1"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v1")) "," (Set (Var "w")))) "implies" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "w"))) ")" & (Bool "(" "not" (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v")) "," (Set (Var "v1"))) "or" (Bool (Set (Var "v")) "," (Set (Var "v1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u")) "," (Set (Var "u1"))) "or" (Bool (Set (Var "v")) "," (Set (Var "v1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "u"))) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "ex" (Set (Var "u1")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_hidden :::"<>"::: ) (Set (Var "u1"))) & (Bool (Set (Var "w")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u")) "," (Set (Var "v"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "ex" (Set (Var "u1")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_hidden :::"<>"::: ) (Set (Var "u1"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "w")) "," (Set (Var "u1"))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"Oriented_Orthogonality_Space-like"::: DIRORT:def 1 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_dirort :::"Oriented_Orthogonality_Space-like"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "u")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v")) "," (Set (Var "w"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "w")) "," (Set (Var "w"))) & "(" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "v1"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v1")) "," (Set (Var "u1"))) & (Bool (Bool "not" (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "v"))))) "implies" (Bool (Set (Var "u1")) ($#r1_hidden :::"="::: ) (Set (Var "v1"))) ")" & "(" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "v1"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "w"))) & (Bool (Bool "not" (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v1")) "," (Set (Var "w"))))) "implies" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "w")) "," (Set (Var "v1"))) ")" & "(" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "v1")))) "implies" (Bool (Set (Var "v")) "," (Set (Var "u")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v1")) "," (Set (Var "u1"))) ")" & "(" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "v1"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v1")) "," (Set (Var "w")))) "implies" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "w"))) ")" & (Bool "(" "not" (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v")) "," (Set (Var "v1"))) "or" (Bool (Set (Var "v")) "," (Set (Var "v1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u")) "," (Set (Var "u1"))) "or" (Bool (Set (Var "v")) "," (Set (Var "v1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "u"))) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "ex" (Set (Var "u1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_hidden :::"<>"::: ) (Set (Var "u1"))) & (Bool (Set (Var "w")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u")) "," (Set (Var "v"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "ex" (Set (Var "u1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_hidden :::"<>"::: ) (Set (Var "u1"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "w")) "," (Set (Var "u1"))) ")" )) ")" ) ")" ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_dirort :::"Oriented_Orthogonality_Space-like"::: ) for ($#l1_analoaf :::"AffinStruct"::: ) ; end; definitionmode Oriented_Orthogonality_Space is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_dirort :::"Oriented_Orthogonality_Space-like"::: ) ($#l1_analoaf :::"AffinStruct"::: ) ; end; theorem :: DIRORT:3 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool (Set ($#k6_analort :::"CMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ) "is" ($#l1_analoaf :::"Oriented_Orthogonality_Space":::)))) ; theorem :: DIRORT:4 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool (Set ($#k5_analort :::"CESpace"::: ) "(" (Set (Var "V")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ) "is" ($#l1_analoaf :::"Oriented_Orthogonality_Space":::)))) ; theorem :: DIRORT:5 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"Oriented_Orthogonality_Space":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "ex" (Set (Var "u1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "u1")) "," (Set (Var "w")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u")) "," (Set (Var "v"))) & (Bool (Set (Var "u1")) ($#r1_hidden :::"<>"::: ) (Set (Var "w"))) ")" )))) ; theorem :: DIRORT:6 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"Oriented_Orthogonality_Space":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "ex" (Set (Var "u1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "u1"))) & (Bool "(" (Bool (Set (Var "v")) "," (Set (Var "w")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u")) "," (Set (Var "u1"))) "or" (Bool (Set (Var "v")) "," (Set (Var "w")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "u"))) ")" ) ")" )))) ; definitionlet "AS" be ($#l1_analoaf :::"Oriented_Orthogonality_Space":::); let "a", "b", "c", "d" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AS")); pred "a" "," "b" :::"_|_"::: "c" "," "d" means :: DIRORT:def 2 (Bool "(" (Bool "a" "," "b" ($#r2_analoaf :::"'//'"::: ) "c" "," "d") "or" (Bool "a" "," "b" ($#r2_analoaf :::"'//'"::: ) "d" "," "c") ")" ); end; :: deftheorem defines :::"_|_"::: DIRORT:def 2 : (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"Oriented_Orthogonality_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_dirort :::"_|_"::: ) (Set (Var "c")) "," (Set (Var "d"))) "iff" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "c")) "," (Set (Var "d"))) "or" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "d")) "," (Set (Var "c"))) ")" ) ")" ))); definitionlet "AS" be ($#l1_analoaf :::"Oriented_Orthogonality_Space":::); let "a", "b", "c", "d" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "AS")); pred "a" "," "b" :::"//"::: "c" "," "d" means :: DIRORT:def 3 (Bool "ex" (Set (Var "e")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"Element":::) "of" "AS" "st" (Bool "(" (Bool (Set (Var "e")) ($#r1_hidden :::"<>"::: ) (Set (Var "f"))) & (Bool (Set (Var "e")) "," (Set (Var "f")) ($#r2_analoaf :::"'//'"::: ) "a" "," "b") & (Bool (Set (Var "e")) "," (Set (Var "f")) ($#r2_analoaf :::"'//'"::: ) "c" "," "d") ")" )); end; :: deftheorem defines :::"//"::: DIRORT:def 3 : (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"Oriented_Orthogonality_Space":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_dirort :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) "iff" (Bool "ex" (Set (Var "e")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "e")) ($#r1_hidden :::"<>"::: ) (Set (Var "f"))) & (Bool (Set (Var "e")) "," (Set (Var "f")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "e")) "," (Set (Var "f")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" )) ")" ))); definitionlet "IT" be ($#l1_analoaf :::"Oriented_Orthogonality_Space":::); attr "IT" is :::"bach_transitive"::: means :: DIRORT:def 4 (Bool "for" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "w")) "," (Set (Var "w1")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v")) "," (Set (Var "v1"))) & (Bool (Set (Var "w")) "," (Set (Var "w1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v")) "," (Set (Var "v1"))) & (Bool (Set (Var "w")) "," (Set (Var "w1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u2")) "," (Set (Var "v2"))) & (Bool (Bool "not" (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Var "w1")))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "v1"))))) "holds" (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u2")) "," (Set (Var "v2")))); end; :: deftheorem defines :::"bach_transitive"::: DIRORT:def 4 : (Bool "for" (Set (Var "IT")) "being" ($#l1_analoaf :::"Oriented_Orthogonality_Space":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_dirort :::"bach_transitive"::: ) ) "iff" (Bool "for" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "w")) "," (Set (Var "w1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v")) "," (Set (Var "v1"))) & (Bool (Set (Var "w")) "," (Set (Var "w1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v")) "," (Set (Var "v1"))) & (Bool (Set (Var "w")) "," (Set (Var "w1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u2")) "," (Set (Var "v2"))) & (Bool (Bool "not" (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Var "w1")))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "v1"))))) "holds" (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u2")) "," (Set (Var "v2")))) ")" )); definitionlet "IT" be ($#l1_analoaf :::"Oriented_Orthogonality_Space":::); attr "IT" is :::"right_transitive"::: means :: DIRORT:def 5 (Bool "for" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "w")) "," (Set (Var "w1")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v")) "," (Set (Var "v1"))) & (Bool (Set (Var "v")) "," (Set (Var "v1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "w")) "," (Set (Var "w1"))) & (Bool (Set (Var "u2")) "," (Set (Var "v2")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "w")) "," (Set (Var "w1"))) & (Bool (Bool "not" (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Var "w1")))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "v1"))))) "holds" (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u2")) "," (Set (Var "v2")))); end; :: deftheorem defines :::"right_transitive"::: DIRORT:def 5 : (Bool "for" (Set (Var "IT")) "being" ($#l1_analoaf :::"Oriented_Orthogonality_Space":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_dirort :::"right_transitive"::: ) ) "iff" (Bool "for" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "w")) "," (Set (Var "w1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v")) "," (Set (Var "v1"))) & (Bool (Set (Var "v")) "," (Set (Var "v1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "w")) "," (Set (Var "w1"))) & (Bool (Set (Var "u2")) "," (Set (Var "v2")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "w")) "," (Set (Var "w1"))) & (Bool (Bool "not" (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Var "w1")))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "v1"))))) "holds" (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u2")) "," (Set (Var "v2")))) ")" )); definitionlet "IT" be ($#l1_analoaf :::"Oriented_Orthogonality_Space":::); attr "IT" is :::"left_transitive"::: means :: DIRORT:def 6 (Bool "for" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "w")) "," (Set (Var "w1")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v")) "," (Set (Var "v1"))) & (Bool (Set (Var "v")) "," (Set (Var "v1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "w")) "," (Set (Var "w1"))) & (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u2")) "," (Set (Var "v2"))) & (Bool (Bool "not" (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "u1")))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "v1"))))) "holds" (Bool (Set (Var "u2")) "," (Set (Var "v2")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "w")) "," (Set (Var "w1")))); end; :: deftheorem defines :::"left_transitive"::: DIRORT:def 6 : (Bool "for" (Set (Var "IT")) "being" ($#l1_analoaf :::"Oriented_Orthogonality_Space":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_dirort :::"left_transitive"::: ) ) "iff" (Bool "for" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "w")) "," (Set (Var "w1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v")) "," (Set (Var "v1"))) & (Bool (Set (Var "v")) "," (Set (Var "v1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "w")) "," (Set (Var "w1"))) & (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u2")) "," (Set (Var "v2"))) & (Bool (Bool "not" (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "u1")))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "v1"))))) "holds" (Bool (Set (Var "u2")) "," (Set (Var "v2")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "w")) "," (Set (Var "w1")))) ")" )); definitionlet "IT" be ($#l1_analoaf :::"Oriented_Orthogonality_Space":::); attr "IT" is :::"Euclidean_like"::: means :: DIRORT:def 7 (Bool "for" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v")) "," (Set (Var "v1")))) "holds" (Bool (Set (Var "v")) "," (Set (Var "v1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "u")))); end; :: deftheorem defines :::"Euclidean_like"::: DIRORT:def 7 : (Bool "for" (Set (Var "IT")) "being" ($#l1_analoaf :::"Oriented_Orthogonality_Space":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_dirort :::"Euclidean_like"::: ) ) "iff" (Bool "for" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v")) "," (Set (Var "v1")))) "holds" (Bool (Set (Var "v")) "," (Set (Var "v1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u1")) "," (Set (Var "u")))) ")" )); definitionlet "IT" be ($#l1_analoaf :::"Oriented_Orthogonality_Space":::); attr "IT" is :::"Minkowskian_like"::: means :: DIRORT:def 8 (Bool "for" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v")) "," (Set (Var "v1")))) "holds" (Bool (Set (Var "v")) "," (Set (Var "v1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u")) "," (Set (Var "u1")))); end; :: deftheorem defines :::"Minkowskian_like"::: DIRORT:def 8 : (Bool "for" (Set (Var "IT")) "being" ($#l1_analoaf :::"Oriented_Orthogonality_Space":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_dirort :::"Minkowskian_like"::: ) ) "iff" (Bool "for" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v")) "," (Set (Var "v1")))) "holds" (Bool (Set (Var "v")) "," (Set (Var "v1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u")) "," (Set (Var "u1")))) ")" )); theorem :: DIRORT:7 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"Oriented_Orthogonality_Space":::) (Bool "for" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "holds" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_dirort :::"//"::: ) (Set (Var "w")) "," (Set (Var "w"))) & (Bool (Set (Var "w")) "," (Set (Var "w")) ($#r2_dirort :::"//"::: ) (Set (Var "u")) "," (Set (Var "u1"))) ")" ))) ; theorem :: DIRORT:8 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"Oriented_Orthogonality_Space":::) (Bool "for" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_dirort :::"//"::: ) (Set (Var "v")) "," (Set (Var "v1")))) "holds" (Bool (Set (Var "v")) "," (Set (Var "v1")) ($#r2_dirort :::"//"::: ) (Set (Var "u")) "," (Set (Var "u1"))))) ; theorem :: DIRORT:9 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"Oriented_Orthogonality_Space":::) (Bool "for" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_dirort :::"//"::: ) (Set (Var "v")) "," (Set (Var "v1")))) "holds" (Bool (Set (Var "u1")) "," (Set (Var "u")) ($#r2_dirort :::"//"::: ) (Set (Var "v1")) "," (Set (Var "v"))))) ; theorem :: DIRORT:10 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"Oriented_Orthogonality_Space":::) "holds" (Bool "(" (Bool (Set (Var "AS")) "is" ($#v4_dirort :::"left_transitive"::: ) ) "iff" (Bool "for" (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "w")) "," (Set (Var "w1")) "," (Set (Var "u2")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "v")) "," (Set (Var "v1")) ($#r2_dirort :::"//"::: ) (Set (Var "u2")) "," (Set (Var "v2"))) & (Bool (Set (Var "v")) "," (Set (Var "v1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "w")) "," (Set (Var "w1"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set (Var "v1")))) "holds" (Bool (Set (Var "u2")) "," (Set (Var "v2")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "w")) "," (Set (Var "w1")))) ")" )) ; theorem :: DIRORT:11 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"Oriented_Orthogonality_Space":::) "holds" (Bool "(" (Bool (Set (Var "AS")) "is" ($#v2_dirort :::"bach_transitive"::: ) ) "iff" (Bool "for" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "v")) "," (Set (Var "v1"))) & (Bool (Set (Var "v")) "," (Set (Var "v1")) ($#r2_dirort :::"//"::: ) (Set (Var "u2")) "," (Set (Var "v2"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set (Var "v1")))) "holds" (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u2")) "," (Set (Var "v2")))) ")" )) ; theorem :: DIRORT:12 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"Oriented_Orthogonality_Space":::) "st" (Bool (Bool (Set (Var "AS")) "is" ($#v2_dirort :::"bach_transitive"::: ) )) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "w")) "," (Set (Var "w1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_dirort :::"//"::: ) (Set (Var "v")) "," (Set (Var "v1"))) & (Bool (Set (Var "v")) "," (Set (Var "v1")) ($#r2_dirort :::"//"::: ) (Set (Var "w")) "," (Set (Var "w1"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set (Var "v1")))) "holds" (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_dirort :::"//"::: ) (Set (Var "w")) "," (Set (Var "w1"))))) ; theorem :: DIRORT:13 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"Oriented_Orthogonality_Space":::) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "AS")) ($#r1_hidden :::"="::: ) (Set ($#k5_analort :::"CESpace"::: ) "(" (Set (Var "V")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "AS")) "is" ($#v5_dirort :::"Euclidean_like"::: ) ) & (Bool (Set (Var "AS")) "is" ($#v4_dirort :::"left_transitive"::: ) ) & (Bool (Set (Var "AS")) "is" ($#v3_dirort :::"right_transitive"::: ) ) & (Bool (Set (Var "AS")) "is" ($#v2_dirort :::"bach_transitive"::: ) ) ")" )))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_dirort :::"Oriented_Orthogonality_Space-like"::: ) ($#v2_dirort :::"bach_transitive"::: ) ($#v3_dirort :::"right_transitive"::: ) ($#v4_dirort :::"left_transitive"::: ) ($#v5_dirort :::"Euclidean_like"::: ) for ($#l1_analoaf :::"AffinStruct"::: ) ; end; theorem :: DIRORT:14 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"Oriented_Orthogonality_Space":::) "st" (Bool (Bool ($#r1_analmetr :::"Gen"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "AS")) ($#r1_hidden :::"="::: ) (Set ($#k6_analort :::"CMSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "AS")) "is" ($#v6_dirort :::"Minkowskian_like"::: ) ) & (Bool (Set (Var "AS")) "is" ($#v4_dirort :::"left_transitive"::: ) ) & (Bool (Set (Var "AS")) "is" ($#v3_dirort :::"right_transitive"::: ) ) & (Bool (Set (Var "AS")) "is" ($#v2_dirort :::"bach_transitive"::: ) ) ")" )))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_dirort :::"Oriented_Orthogonality_Space-like"::: ) ($#v2_dirort :::"bach_transitive"::: ) ($#v3_dirort :::"right_transitive"::: ) ($#v4_dirort :::"left_transitive"::: ) ($#v6_dirort :::"Minkowskian_like"::: ) for ($#l1_analoaf :::"AffinStruct"::: ) ; end; theorem :: DIRORT:15 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"Oriented_Orthogonality_Space":::) "st" (Bool (Bool (Set (Var "AS")) "is" ($#v4_dirort :::"left_transitive"::: ) )) "holds" (Bool (Set (Var "AS")) "is" ($#v3_dirort :::"right_transitive"::: ) )) ; theorem :: DIRORT:16 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"Oriented_Orthogonality_Space":::) "st" (Bool (Bool (Set (Var "AS")) "is" ($#v4_dirort :::"left_transitive"::: ) )) "holds" (Bool (Set (Var "AS")) "is" ($#v2_dirort :::"bach_transitive"::: ) )) ; theorem :: DIRORT:17 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"Oriented_Orthogonality_Space":::) "st" (Bool (Bool (Set (Var "AS")) "is" ($#v2_dirort :::"bach_transitive"::: ) )) "holds" (Bool "(" (Bool (Set (Var "AS")) "is" ($#v3_dirort :::"right_transitive"::: ) ) "iff" (Bool "for" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "u2")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u2")) "," (Set (Var "v2"))) & (Bool (Set (Var "v")) "," (Set (Var "v1")) ($#r2_analoaf :::"'//'"::: ) (Set (Var "u2")) "," (Set (Var "v2"))) & (Bool (Set (Var "u2")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2")))) "holds" (Bool (Set (Var "u")) "," (Set (Var "u1")) ($#r2_dirort :::"//"::: ) (Set (Var "v")) "," (Set (Var "v1")))) ")" )) ; theorem :: DIRORT:18 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"Oriented_Orthogonality_Space":::) "st" (Bool (Bool (Set (Var "AS")) "is" ($#v3_dirort :::"right_transitive"::: ) ) & (Bool "(" (Bool (Set (Var "AS")) "is" ($#v5_dirort :::"Euclidean_like"::: ) ) "or" (Bool (Set (Var "AS")) "is" ($#v6_dirort :::"Minkowskian_like"::: ) ) ")" )) "holds" (Bool (Set (Var "AS")) "is" ($#v4_dirort :::"left_transitive"::: ) )) ;