let y be object ; :: thesis: ( y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) implies y in Plane (p,(p1 + p2)) )
assume y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) ; :: thesis: y in Plane (p,(p1 + p2))
then consider x being object such that
A2: ( [x,y] in transl (p1,(TOP-REAL n)) & x in Plane (p,p2) ) by RELAT_1:def 13;
consider x1 being Point of (TOP-REAL n) such that
A3: ( x = x1 & |(p,(x1 - p2))| = 0 ) by A2;
A4: y = (transl (p1,(TOP-REAL n))) . x1 by A2, A3, FUNCT_1:1
.= p1 + x1 by RLTOPSP1:def 10 ;
( x in dom (transl (p1,(TOP-REAL n))) & y = (transl (p1,(TOP-REAL n))) . x ) by A2, FUNCT_1:1;
then y in rng (transl (p1,(TOP-REAL n))) by FUNCT_1:3;
then reconsider y1 = y as Point of (TOP-REAL n) ;
x1 - p2 = (x1 - p2) + (0. (TOP-REAL n)) by RLVECT_1:4
.= (x1 - p2) + (p1 + (- p1)) by RLVECT_1:5
.= ((x1 + (- p2)) + p1) + (- p1) by RLVECT_1:def 3
.= (y1 - p2) - p1 by A4, RLVECT_1:def 3
.= y1 - (p1 + p2) by RLVECT_1:27 ;
hence y in Plane (p,(p1 + p2)) by A3; :: thesis: verum

let y be object ; :: thesis: ( y in Plane (p,(p1 + p2)) implies y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) )
assume y in Plane (p,(p1 + p2)) ; :: thesis: y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2))
then consider y1 being Point of (TOP-REAL n) such that
A5: ( y = y1 & |(p,(y1 - (p1 + p2)))| = 0 ) ;
set x = y1 - p1;
y1 - p1 in the carrier of (TOP-REAL n) ;
then A6: y1 - p1 in dom (transl (p1,(TOP-REAL n))) by FUNCT_2:def 1;
p1 + (y1 - p1) = y1 by RLVECT_4:1;
then (transl (p1,(TOP-REAL n))) . (y1 - p1) = y1 by RLTOPSP1:def 10;
then A7: [(y1 - p1),y1] in transl (p1,(TOP-REAL n)) by A6, FUNCT_1:1;
(y1 - p1) - p2 = y1 - (p1 + p2) by RLVECT_1:27;
then y1 - p1 in Plane (p,p2) by A5;
hence y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) by A5, A7, RELAT_1:def 13; :: thesis: verum