Using the point T_b and the point I, construct a line s_b (rule W02);

% DET: points T_b and I are not the same

Using the point T_c and the point I, construct a line s_c (rule W02);

% DET: points T_c and I are not the same

Using the point T_b, the point I and the point T_c, construct a circle circle[T_b,T_c,angle[c][b]] (rule W20);

% NDG: points T_b and I are not the same points I and T_c are not the same points T_b and T_c are not the same

Using the point T_b, the point I and the point T_c, construct a circle circle[T_c,I,angle[c][s[a]]] (rule W20);

% NDG: points T_b and I are not the same points I and T_c are not the same points T_c and I are not the same

Using the circle circle[T_c,I,angle[c][s[a]]] and the circle circle[T_b,T_c,angle[c][b]], construct a point A_c2 and a point A (rule W07);

% NDG: circles circle[T_c,I,angle[c][s[a]]] and circle[T_b,T_c,angle[c][b]] intersect

% DET: circles circle[T_c,I,angle[c][s[a]]] and circle[T_b,T_c,angle[c][b]] are not the same

Using the point A and the point T_b, construct a line b (rule W02);

% DET: points A and T_b are not the same

Using the point T_c and the point A, construct a line c (rule W02);

% DET: points T_c and A are not the same

Using the line s_b and the line c, construct a point B (rule W03);

% NDG: lines s_b and c are not parallel

% DET: lines s_b and c are not the same

Using the line s_c and the line b, construct a point C (rule W03);

% NDG: lines s_c and b are not parallel

% DET: lines s_c and b are not the same