theorem Th38: :: EUCLID12:50

for A, B, C being Point of (TOP-REAL 2)
for L1, L2 being Element of line_of_REAL 2 st L1 _|_ L2 & C in L1 /\ L2 & A in L1 & B in L2 & A <> C & B <> C & not angle (A,C,B) = PI / 2 holds
angle (A,C,B) = (3 * PI) / 2