let V be RealLinearSpace; :: thesis: for M, N1, N2 being non empty Affine Subset of V st N1 is Subspace-like & N2 is Subspace-like & M is_parallel_to N1 & M is_parallel_to N2 holds
N1 = N2
let M, N1, N2 be non empty Affine Subset of V; :: thesis: ( N1 is Subspace-like & N2 is Subspace-like & M is_parallel_to N1 & M is_parallel_to N2 implies N1 = N2 )
assume that
A1: N1 is Subspace-like and
A2: N2 is Subspace-like and
A3: M is_parallel_to N1 and
A4: M is_parallel_to N2 ; :: thesis: N1 = N2
N1 is_parallel_to M by A3, Th2;
then N1 is_parallel_to N2 by A4, Th3;
then consider v1 being VECTOR of V such that
A5: N1 = N2 + {v1} by Def1;
0. V in N1 by A1, RUSUB_4:def 8;
then 0. V in { (p + q) where p, q is Element of V : ( p in N2 & q in {v1} ) } by A5, RUSUB_4:def 10;
then consider p1, q1 being Element of V such that
A6: ( 0. V = p1 + q1 & p1 in N2 & q1 in {v1} ) ;
0. V = p1 + v1 by A6, TARSKI:def 1;
then A7: - v1 in N2 by A6, RLVECT_1:19;
v1 = - (- v1) by RLVECT_1:30
.= (- 1) * (- v1) by RLVECT_1:29 ;
then v1 in N2 by A2, A7, RUSUB_4:def 8;
then A8: N1 c= N2 by A2, A5, Th13;
N2 is_parallel_to M by A4, Th2;
then N2 is_parallel_to N1 by A3, Th3;
then consider v2 being VECTOR of V such that
A9: N2 = N1 + {v2} by Def1;
0. V in N2 by A2, RUSUB_4:def 8;
then 0. V in { (p + q) where p, q is Element of V : ( p in N1 & q in {v2} ) } by A9, RUSUB_4:def 10;
then consider p2, q2 being Element of V such that
A10: ( 0. V = p2 + q2 & p2 in N1 & q2 in {v2} ) ;
0. V = p2 + v2 by A10, TARSKI:def 1;
then A11: - v2 in N1 by A10, RLVECT_1:19;
v2 = - (- v2) by RLVECT_1:30
.= (- 1) * (- v2) by RLVECT_1:29 ;
then v2 in N1 by A1, A11, RUSUB_4:def 8;
then N2 c= N1 by A1, A9, Th13;
hence N1 = N2 by A8, XBOOLE_0:def 10; :: thesis: verum