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;

hence ( angle (A,C,B) = PI / 2 or angle (A,C,B) = (3 * PI) / 2 ) by A5, EUCLID_3:45; :: thesis: verum

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) )

then
|((A - C),(B - C))| = 0
by A1, Th36;
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;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

hence ( angle (A,C,B) = PI / 2 or angle (A,C,B) = (3 * PI) / 2 ) by A5, EUCLID_3:45; :: thesis: verum