Using the point T_a and the point I, construct a line s_a (rule W02);

% DET: points T_a and I are not the same

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_a, the point I and the point T_b, construct a circle circle[T_a,T_b,angle[b][a]] (rule W20);

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

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

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

Using the circle circle[T_b,I,angle[b][s[c]]] and the circle circle[T_a,T_b,angle[b][a]], construct a point C_c1 and a point C (rule W07);

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

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

Using the point C and the point T_a, construct a line a (rule W02);

% DET: points C and T_a are not the same

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

% DET: points T_b and C are not the same

Using the line s_a and the line b, construct a point A (rule W03);

% NDG: lines s_a and b are not parallel

% DET: lines s_a and b are not the same

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

% NDG: lines s_b and a are not parallel

% DET: lines s_b and a are not the same