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