let n be Element of NAT ; :: thesis: 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; :: thesis: ( P1 is being_plane & P1 c= P2 implies P1 = P2 )
assume that
A1: P1 is being_plane and
A2: P1 c= P2 ; :: thesis: 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, Def10;
A4: x3 in plane x1,x2,x3 by Th87;
( x1 in plane x1,x2,x3 & x2 in plane x1,x2,x3 ) by Th87;
hence P1 = P2 by A2, A3, A4, Th97; :: thesis: verum