let V be non empty right_complementable add-associative right_zeroed RLSStruct ; for M, N being Affine Subset of V st M is_parallel_to N holds
N is_parallel_to M
let M, N be Affine Subset of V; ( M is_parallel_to N implies N is_parallel_to M )
assume
M is_parallel_to N
; N is_parallel_to M
then consider w1 being VECTOR of V such that
A1:
M = N + {w1}
;
set w2 = - w1;
for x being object st x in N holds
x in M + {(- w1)}
then A5:
N c= M + {(- w1)}
;
take
- w1
; RUSUB_5:def 1 N = M + {(- w1)}
for x being object st x in M + {(- w1)} holds
x in N
proof
let x be
object ;
( x in M + {(- w1)} implies x in N )
assume A6:
x in M + {(- w1)}
;
x in N
then
x in { (u + v) where u, v is Element of V : ( u in M & v in {(- w1)} ) }
by RUSUB_4:def 9;
then consider u9,
v9 being
Element of
V such that A7:
x = u9 + v9
and A8:
u9 in M
and A9:
v9 in {(- w1)}
;
reconsider x =
x as
Element of
V by A6;
x = u9 + (- w1)
by A7, A9, TARSKI:def 1;
then
x + w1 = u9 + ((- w1) + w1)
by RLVECT_1:def 3;
then A10:
x + w1 = u9 + (0. V)
by RLVECT_1:5;
u9 in { (u + v) where u, v is Element of V : ( u in N & v in {w1} ) }
by A1, A8, RUSUB_4:def 9;
then consider u1,
v1 being
Element of
V such that A11:
(
u9 = u1 + v1 &
u1 in N )
and A12:
v1 in {w1}
;
w1 = v1
by A12, TARSKI:def 1;
hence
x in N
by A10, A11, RLVECT_1:8;
verum
end;
then
M + {(- w1)} c= N
;
hence
N = M + {(- w1)}
by A5; verum