let n be Nat; for P1, P2 being Element of plane_of_REAL n st P1 is being_plane & P1 c= P2 holds
P1 = P2
let P1, P2 be Element of plane_of_REAL n; ( P1 is being_plane & P1 c= P2 implies P1 = P2 )
assume that
A1:
P1 is being_plane
and
A2:
P1 c= P2
; P1 = P2
consider x1, x2, x3 being Element of REAL n such that
A3:
( x2 - x1,x3 - x1 are_lindependent2 & P1 = plane (x1,x2,x3) )
by A1;
A4:
x3 in plane (x1,x2,x3)
by Th82;
( x1 in plane (x1,x2,x3) & x2 in plane (x1,x2,x3) )
by Th82;
hence
P1 = P2
by A2, A3, A4, Th92; verum