let L1, L2 be Element of line_of_REAL 2; ( L1 // L2 or ex x being Element of REAL 2 st
( L1 = {x} or L2 = {x} ) or ( L1 is being_line & L2 is being_line & ex x being Element of REAL 2 st L1 /\ L2 = {x} ) )
assume A1:
not L1 // L2
; ( ex x being Element of REAL 2 st
( L1 = {x} or L2 = {x} ) or ( L1 is being_line & L2 is being_line & ex x being Element of REAL 2 st L1 /\ L2 = {x} ) )
set n = 2;
consider x1, x2 being Element of REAL 2 such that
A2:
L1 = Line (x1,x2)
by EUCLIDLP:51;
consider y1, y2 being Element of REAL 2 such that
A3:
L2 = Line (y1,y2)
by EUCLIDLP:51;
( x2 - x1 = 0* 2 or y2 - y1 = 0* 2 or for r being Real holds not x2 - x1 = r * (y2 - y1) )
by A1, A2, A3, EUCLIDLP:def 7, EUCLIDLP:def 1;
per cases then
( x1 = x2 or y1 = y2 or ( not x1 = x2 & y1 <> y2 & ( for r being Real holds x2 - x1 <> r * (y2 - y1) ) ) )
by EUCLIDLP:9;
suppose A4:
( not
x1 = x2 &
y1 <> y2 & ( for
r being
Real holds
x2 - x1 <> r * (y2 - y1) ) )
;
( ex x being Element of REAL 2 st
( L1 = {x} or L2 = {x} ) or ( L1 is being_line & L2 is being_line & ex x being Element of REAL 2 st L1 /\ L2 = {x} ) )
x2 - x1,
y2 - y1 are_lindependent2
then consider Pt being
Element of
REAL 2
such that A5:
Pt in L1
and A6:
Pt in L2
by A2, A3, Th13, EUCLIDLP:114, EUCLIDLP:49;
A7:
{Pt} c= L1 /\ L2
L1 /\ L2 c= {Pt}
proof
let t be
object ;
TARSKI:def 3 ( not t in L1 /\ L2 or t in {Pt} )
assume A8:
t in L1 /\ L2
;
t in {Pt}
assume
not
t in {Pt}
;
contradiction
then A9:
t <> Pt
by TARSKI:def 1;
reconsider t1 =
t as
Element of
REAL 2
by A8;
(
t1 in L1 &
t1 in L2 &
Pt in L1 &
Pt in L2 )
by A8, A5, A6, XBOOLE_0:def 4;
then
(
Line (
t1,
Pt)
= L1 &
Line (
t1,
Pt)
= L2 )
by A2, A3, A9, EUCLID_4:10, EUCLID_4:11;
then
(
L1 = L2 &
L1 is
being_line &
L2 is
being_line )
by A2, A4;
hence
contradiction
by A1, EUCLIDLP:65;
verum
end; then
L1 /\ L2 = {Pt}
by A7;
hence
( ex
x being
Element of
REAL 2 st
(
L1 = {x} or
L2 = {x} ) or (
L1 is
being_line &
L2 is
being_line & ex
x being
Element of
REAL 2 st
L1 /\ L2 = {x} ) )
by A4, A2, A3;
verum end; end;