TheoremsclosedInterior_eq_affineSegment, closedInterior_face_eq_affineSegment, interior_eq_image_Ioo, mem_closedInterior_face_iff_wbtw, mem_closedInterior_iff_wbtw, mem_interior_face_iff_sbtw, mem_interior_iff_sbtw, sbtw_map_iff, wbtw_map_iff, not_wbtw_of_injective, mem_of_wbtw, right_mem_of_wbtw, wbtw_or_wbtw_or_wbtw, mem_of_wbtw, sbtw_map_iff, wbtw_map_iff, add_const, affineCombination_of_mem_affineSpan_pair, const_add, const_sub, const_vadd, const_vsub, left_mem_affineSpan, left_mem_image_Ioi, left_ne, left_ne_right, mem_image_Ioo, ne_left, ne_right, neg, not_rotate, not_swap_left, not_swap_right, of_lt_of_lt, right_mem_affineSpan, right_mem_image_Ioi, right_ne, sub_const, trans_expand_left, trans_expand_right, trans_left, trans_left_right, trans_right, trans_right_left, trans_wbtw_left_ne, trans_wbtw_right_ne, vadd_const, vsub_const, wbtw, sbtw_map_iff, wbtw_map_iff, add_const, collinear, const_add, const_sub, const_vadd, const_vsub, left_mem_affineSpan_of_right_ne, left_mem_image_Ici_of_right_ne, left_ne_right_of_ne_left, left_ne_right_of_ne_right, map, mem_affineSpan, mem_segment, neg, of_le_of_le, right_mem_affineSpan_of_left_ne, right_mem_image_Ici_of_left_ne, rotate_iff, sameRay_vsub, sameRay_vsub_left, sameRay_vsub_right, sub_const, swap_left_iff, swap_right_iff, trans_expand_left, trans_expand_right, trans_left, trans_left_ne, trans_left_right, trans_right, trans_right_left, trans_right_ne, trans_sbtw_left, trans_sbtw_right, vadd_const, vsub_const, affineSegment_comm, affineSegment_const_vadd_image, affineSegment_const_vsub_image, affineSegment_eq_segment, affineSegment_image, affineSegment_same, affineSegment_subset_affineSpan, affineSegment_vadd_const_image, affineSegment_vsub_const_image, left_mem_affineSegment, mem_const_vadd_affineSegment, mem_const_vsub_affineSegment, mem_segment_iff_wbtw, mem_vadd_const_affineSegment, mem_vsub_const_affineSegment, not_sbtw_self, not_sbtw_self_left, not_sbtw_self_right, right_mem_affineSegment, sbtw_add_const_iff, sbtw_comm, sbtw_const_add_iff, sbtw_const_sub_iff, sbtw_const_vadd_iff, sbtw_const_vsub_iff, sbtw_iff_left_ne_and_right_mem_image_Ioi, sbtw_iff_mem_image_Ioo_and_ne, sbtw_iff_right_ne_and_left_mem_image_Ioi, sbtw_lineMap_iff, sbtw_midpoint_of_ne, sbtw_mul_sub_add_iff, sbtw_neg_iff, sbtw_of_sbtw_of_sbtw_of_mem_affineSpan_pair, sbtw_one_zero_iff, sbtw_pointReflection_of_ne, sbtw_sub_const_iff, sbtw_vadd_const_iff, sbtw_vsub_const_iff, sbtw_zero_one_iff, wbtw_add_const_iff, wbtw_comm, wbtw_const_add_iff, wbtw_const_sub_iff, wbtw_const_vadd_iff, wbtw_const_vsub_iff, wbtw_iff_left_eq_or_right_mem_image_Ici, wbtw_iff_of_le, wbtw_iff_right_eq_or_left_mem_image_Ici, wbtw_iff_sameRay_vsub, wbtw_lineMap_iff, wbtw_midpoint, wbtw_mul_sub_add_iff, wbtw_neg_iff, wbtw_one_zero_iff, wbtw_or_wbtw_smul_vadd_of_nonneg, wbtw_or_wbtw_smul_vadd_of_nonpos, wbtw_pointReflection, wbtw_rotate_iff, wbtw_self_iff, wbtw_self_left, wbtw_self_right, wbtw_smul_vadd_smul_vadd_of_nonneg_of_le, wbtw_smul_vadd_smul_vadd_of_nonneg_of_nonpos, wbtw_smul_vadd_smul_vadd_of_nonpos_of_le, wbtw_smul_vadd_smul_vadd_of_nonpos_of_nonneg, wbtw_sub_const_iff, wbtw_swap_left_iff, wbtw_swap_right_iff, wbtw_total_of_sameRay_vsub_left, wbtw_vadd_const_iff, wbtw_vsub_const_iff, wbtw_zero_one_iff | 159 |