let A, B, C be Point of (TOP-REAL 2); :: thesis: 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
let L1, L2 be Element of line_of_REAL 2; :: thesis: ( L1 _|_ L2 & C in L1 /\ L2 & A in L1 & B in L2 & A <> C & B <> C & not angle (A,C,B) = PI / 2 implies angle (A,C,B) = (3 * PI) / 2 )
assume that
A1: L1 _|_ L2 and
A2: C in L1 /\ L2 and
A3: A in L1 and
A4: B in L2 and
A5: ( A <> C & B <> C ) ; :: thesis: ( angle (A,C,B) = PI / 2 or angle (A,C,B) = (3 * PI) / 2 )
A6: ( C in L1 & C in L2 ) by A2, XBOOLE_0:def 4;

now :: thesis: ( L1 = Line (C,A) & L2 = Line (C,B) )

L1 is being_line by A1, EUCLIDLP:67;
hence L1 = Line (C,A) by A3, A5, A6, Th37; :: thesis: L2 = Line (C,B)
L2 is being_line by A1, EUCLIDLP:67;
hence L2 = Line (C,B) by A4, A5, A6, Th37; :: thesis: verum

end;

then |((A - C),(B - C))| = 0 by A1, Th36;
hence ( angle (A,C,B) = PI / 2 or angle (A,C,B) = (3 * PI) / 2 ) by A5, EUCLID_3:45; :: thesis: verum