let n be Nat; for L1, L2 being Element of line_of_REAL n
for P1, P2 being Element of plane_of_REAL n st L1 is being_line & L2 is being_line & L1 <> L2 & L1 c= P1 & L2 c= P1 & L1 c= P2 & L2 c= P2 holds
P1 = P2
let L1, L2 be Element of line_of_REAL n; for P1, P2 being Element of plane_of_REAL n st L1 is being_line & L2 is being_line & L1 <> L2 & L1 c= P1 & L2 c= P1 & L1 c= P2 & L2 c= P2 holds
P1 = P2
let P1, P2 be Element of plane_of_REAL n; ( L1 is being_line & L2 is being_line & L1 <> L2 & L1 c= P1 & L2 c= P1 & L1 c= P2 & L2 c= P2 implies P1 = P2 )
assume that
A1:
L1 is being_line
and
A2:
L2 is being_line
and
A3:
L1 <> L2
and
A4:
( L1 c= P1 & L2 c= P1 )
and
A5:
( L1 c= P2 & L2 c= P2 )
; P1 = P2
consider x being Element of REAL n such that
A6:
x in L1
and
A7:
not x in L2
by A1, A2, A3, Th79;
consider x1, x2 being Element of REAL n such that
A8:
L2 = Line (x1,x2)
and
A9:
x - x1,x2 - x1 are_lindependent2
by A2, A7, Th55;
A10:
( x1 in L2 & x2 in L2 )
by A8, EUCLID_4:9;
then
P2 = plane (x1,x,x2)
by A5, A6, A9, Th92;
hence
P1 = P2
by A4, A6, A9, A10, Th92; verum