let A, B, C be 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
let L1, L2 be Element of line_of_REAL 2; ( 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 )
; ( 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 ( 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;
L2 = Line (C,B)
L2 is
being_line
by A1, EUCLIDLP:67;
hence
L2 = Line (
C,
B)
by A4, A5, A6, Th37;
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; verum