let n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum