let A, B, C be Point of (TOP-REAL 2); ( A,B,C is_a_triangle implies ex D being Point of (TOP-REAL 2) st
( (median (A,B,C)) /\ (median (B,C,A)) = {D} & (median (B,C,A)) /\ (median (C,A,B)) = {D} & (median (C,A,B)) /\ (median (A,B,C)) = {D} ) )
assume A1:
A,B,C is_a_triangle
; ex D being Point of (TOP-REAL 2) st
( (median (A,B,C)) /\ (median (B,C,A)) = {D} & (median (B,C,A)) /\ (median (C,A,B)) = {D} & (median (C,A,B)) /\ (median (A,B,C)) = {D} )
then consider D being Point of (TOP-REAL 2) such that
A2:
D in median (A,B,C)
and
A3:
D in median (B,C,A)
and
A4:
D in median (C,A,B)
by Th62;
A5:
A,B,C are_mutually_distinct
by A1, EUCLID_6:20;
reconsider rA = A, rB = B, rC = C, rBC = the_midpoint_of_the_segment (B,C), rCA = the_midpoint_of_the_segment (C,A), rAB = the_midpoint_of_the_segment (A,B) as Element of REAL 2 by EUCLID:22;
reconsider L1 = Line (rA,rBC), L2 = Line (rB,rCA), L3 = Line (rC,rAB) as Element of line_of_REAL 2 by EUCLIDLP:47;
A6:
( B,C,A is_a_triangle & C,B,A is_a_triangle )
by A1, MENELAUS:15;
A7:
C,A,B is_a_triangle
by A1, MENELAUS:15;
A8:
( L1 = Line (A,(the_midpoint_of_the_segment (B,C))) & L2 = Line (B,(the_midpoint_of_the_segment (C,A))) & L3 = Line (C,(the_midpoint_of_the_segment (A,B))) )
by Th4;
then A9:
( L1 is being_line & L2 is being_line & L3 is being_line )
by A1, A2, A3, A4, A6, A7, Th61;
( D in L1 & D in L2 & D in L3 )
by A2, A3, A4, Th4;
then A10:
( D in L1 /\ L2 & D in L1 /\ L3 & D in L2 /\ L3 )
by XBOOLE_0:def 4;
now ( not L1 // L2 & L1 is being_line & L2 is being_line & not L1 is being_point & not L2 is being_point )
L1 <> L2
proof
assume A11:
L1 = L2
;
contradiction
A12:
(
A in Line (
A,
(the_midpoint_of_the_segment (B,C))) &
the_midpoint_of_the_segment (
B,
C)
in Line (
A,
(the_midpoint_of_the_segment (B,C))) &
B in Line (
B,
(the_midpoint_of_the_segment (C,A))) &
the_midpoint_of_the_segment (
C,
A)
in Line (
B,
(the_midpoint_of_the_segment (C,A))) &
C in Line (
C,
(the_midpoint_of_the_segment (A,B))) &
the_midpoint_of_the_segment (
A,
B)
in Line (
C,
(the_midpoint_of_the_segment (A,B))) )
by RLTOPSP1:72;
(
A in L1 &
B in L1 &
A in L2 &
B in L2 &
the_midpoint_of_the_segment (
B,
C)
in L1 &
the_midpoint_of_the_segment (
B,
C)
in L2 &
the_midpoint_of_the_segment (
C,
A)
in L1 &
the_midpoint_of_the_segment (
C,
A)
in L2 )
by A12, A11, Th4;
then
L1 = Line (
rA,
rB)
by A5, A9, EUCLIDLP:30;
then A13:
L1 = Line (
A,
B)
by Th4;
(
B <> the_midpoint_of_the_segment (
B,
C) &
B in L1 &
the_midpoint_of_the_segment (
B,
C)
in LSeg (
B,
C) &
the_midpoint_of_the_segment (
B,
C)
in L1 &
L1 is
being_line )
by A2, A8, A1, Th61, RLTOPSP1:72, A11, Th21, A5, Th25;
then
(
A in L1 &
B in L1 &
C in L1 )
by A12, Th4, Th5;
then
C,
A,
B are_collinear
by A13, A5, MENELAUS:13;
hence
contradiction
by A1, MENELAUS:15;
verum
end; hence
not
L1 // L2
by A10, XBOOLE_0:4, EUCLIDLP:71;
( L1 is being_line & L2 is being_line & not L1 is being_point & not L2 is being_point )thus
(
L1 is
being_line &
L2 is
being_line & not
L1 is
being_point & not
L2 is
being_point )
by A8, A1, A2, A3, A6, Th61, Th7;
verum end;
then consider x being Element of REAL 2 such that
A14:
L1 /\ L2 = {x}
by Th16;
now ( not L1 // L3 & L1 is being_line & L3 is being_line & not L1 is being_point & not L3 is being_point )
L1 <> L3
proof
assume A15:
L1 = L3
;
contradiction
A16:
(
A in Line (
A,
(the_midpoint_of_the_segment (B,C))) &
the_midpoint_of_the_segment (
B,
C)
in Line (
A,
(the_midpoint_of_the_segment (B,C))) &
B in Line (
B,
(the_midpoint_of_the_segment (C,A))) &
the_midpoint_of_the_segment (
C,
A)
in Line (
B,
(the_midpoint_of_the_segment (C,A))) &
C in Line (
C,
(the_midpoint_of_the_segment (A,B))) &
the_midpoint_of_the_segment (
A,
B)
in Line (
C,
(the_midpoint_of_the_segment (A,B))) )
by RLTOPSP1:72;
(
A in L1 &
C in L1 &
A in L3 &
C in L3 &
the_midpoint_of_the_segment (
B,
C)
in L1 &
the_midpoint_of_the_segment (
B,
C)
in L3 &
the_midpoint_of_the_segment (
A,
B)
in L1 &
the_midpoint_of_the_segment (
A,
B)
in L3 )
by A15, Th4, A16;
then
L1 = Line (
rA,
rC)
by A5, A9, EUCLIDLP:30;
then A17:
L1 = Line (
A,
C)
by Th4;
(
A <> the_midpoint_of_the_segment (
A,
B) &
A in L1 &
the_midpoint_of_the_segment (
A,
B)
in LSeg (
A,
B) &
the_midpoint_of_the_segment (
A,
B)
in L1 &
L1 is
being_line )
by A2, A5, Th25, A8, A1, Th61, A15, RLTOPSP1:72, Th21;
then
(
A in L1 &
C in L1 &
B in L1 )
by A16, A15, Th4, Th5;
then
B,
A,
C are_collinear
by A17, A5, MENELAUS:13;
hence
contradiction
by A1, MENELAUS:15;
verum
end; hence
not
L1 // L3
by A10, XBOOLE_0:4, EUCLIDLP:71;
( L1 is being_line & L3 is being_line & not L1 is being_point & not L3 is being_point )thus
(
L1 is
being_line &
L3 is
being_line & not
L1 is
being_point & not
L3 is
being_point )
by A2, A4, A8, A1, A7, Th61, Th7;
verum end;
then consider y being Element of REAL 2 such that
A18:
L1 /\ L3 = {y}
by Th16;
now ( not L2 // L3 & L2 is being_line & L3 is being_line & not L2 is being_point & not L3 is being_point )
L2 <> L3
proof
assume A19:
L2 = L3
;
contradiction
A20:
(
A in Line (
A,
(the_midpoint_of_the_segment (B,C))) &
the_midpoint_of_the_segment (
B,
C)
in Line (
A,
(the_midpoint_of_the_segment (B,C))) &
B in Line (
B,
(the_midpoint_of_the_segment (C,A))) &
the_midpoint_of_the_segment (
C,
A)
in Line (
B,
(the_midpoint_of_the_segment (C,A))) &
C in Line (
C,
(the_midpoint_of_the_segment (A,B))) &
the_midpoint_of_the_segment (
A,
B)
in Line (
C,
(the_midpoint_of_the_segment (A,B))) )
by RLTOPSP1:72;
then
(
B in L2 &
C in L2 &
B in L3 &
C in L3 &
rCA in L2 &
rAB in L2 &
rCA in L3 &
rAB in L3 )
by A19, Th4;
then
L2 = Line (
rB,
rC)
by A5, A9, EUCLIDLP:30;
then A21:
L2 = Line (
B,
C)
by Th4;
(
C <> the_midpoint_of_the_segment (
C,
A) &
C in L2 &
the_midpoint_of_the_segment (
C,
A)
in LSeg (
C,
A) &
the_midpoint_of_the_segment (
C,
A)
in L2 &
L2 is
being_line )
by A3, A5, Th25, RLTOPSP1:72, A19, Th21, A6, Th61, A8;
then
(
B in L2 &
C in L2 &
A in L2 )
by A20, Th4, Th5;
hence
contradiction
by A21, A5, A1, MENELAUS:13;
verum
end; hence
not
L2 // L3
by A10, XBOOLE_0:4, EUCLIDLP:71;
( L2 is being_line & L3 is being_line & not L2 is being_point & not L3 is being_point )thus
(
L2 is
being_line &
L3 is
being_line & not
L2 is
being_point & not
L3 is
being_point )
by A3, A4, A8, A6, A7, Th61, Th7;
verum end;
then consider z being Element of REAL 2 such that
A22:
L2 /\ L3 = {z}
by Th16;
( D = x & D = y & D = z )
by A10, A14, A18, A22, TARSKI:def 1;
hence
ex D being Point of (TOP-REAL 2) st
( (median (A,B,C)) /\ (median (B,C,A)) = {D} & (median (B,C,A)) /\ (median (C,A,B)) = {D} & (median (C,A,B)) /\ (median (A,B,C)) = {D} )
by A14, A18, A22, A8; verum