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
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
A5: N2 = N1 + {v2} ;
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
A6: N1 = N2 + {v1} ;
0. V in N2 by A2, RUSUB_4:def 7;
then 0. V in { (p + q) where p, q is Element of V : ( p in N1 & q in {v2} ) } by A5, RUSUB_4:def 9;
then consider p2, q2 being Element of V such that
A7: 0. V = p2 + q2 and
A8: p2 in N1 and
A9: q2 in {v2} ;
0. V = p2 + v2 by A7, A9, TARSKI:def 1;
then A10: - v2 in N1 by A8, RLVECT_1:6;
v2 = - (- v2)
.= (- 1) * (- v2) by RLVECT_1:16 ;
then v2 in N1 by A1, A10, RUSUB_4:def 7;
then A11: N2 c= N1 by A1, A5, Th13;
0. V in N1 by A1, RUSUB_4:def 7;
then 0. V in { (p + q) where p, q is Element of V : ( p in N2 & q in {v1} ) } by A6, RUSUB_4:def 9;
then consider p1, q1 being Element of V such that
A12: 0. V = p1 + q1 and
A13: p1 in N2 and
A14: q1 in {v1} ;
0. V = p1 + v1 by A12, A14, TARSKI:def 1;
then A15: - v1 in N2 by A13, RLVECT_1:6;
v1 = - (- v1)
.= (- 1) * (- v1) by RLVECT_1:16 ;
then v1 in N2 by A2, A15, RUSUB_4:def 7;
then N1 c= N2 by A2, A6, Th13;
hence N1 = N2 by A11; :: thesis: verum