theorem :: EUCLID12:51

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 holds
A,B,C is_a_triangle