let V be non empty right_complementable add-associative right_zeroed RLSStruct ; :: thesis: 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; :: thesis: ( M is_parallel_to N implies N is_parallel_to M )
assume M is_parallel_to N ; :: thesis: N is_parallel_to M
then consider w1 being VECTOR of V such that
A1: M = N + {w1} by Def1;
set w2 = - w1;
for x being set st x in N holds
x in M + {(- w1)}

proof

let x be set ; :: thesis: ( x in N implies x in M + {(- w1)} )
assume A2: x in N ; :: thesis: x in M + {(- w1)}
then reconsider x = x as Element of V ;
A3: w1 in {w1} by TARSKI:def 1;
set y = x + w1;
x + w1 in { (u + v) where u, v is Element of V : ( u in N & v in {w1} ) } by A2, A3;
then A4: x + w1 in M by A1, RUSUB_4:def 10;
x + (w1 + (- w1)) = (x + w1) + (- w1) by RLVECT_1:def 6;
then x + (0. V) = (x + w1) + (- w1) by RLVECT_1:16;
then A5: x = (x + w1) + (- w1) by RLVECT_1:10;
- w1 in {(- w1)} by TARSKI:def 1;
then x in { (u + v) where u, v is Element of V : ( u in M & v in {(- w1)} ) } by A4, A5;
hence x in M + {(- w1)} by RUSUB_4:def 10; :: thesis: verum

end;

then A6: N c= M + {(- w1)} by TARSKI:def 3;
for x being set st x in M + {(- w1)} holds
x in N

proof

let x be set ; :: thesis: ( x in M + {(- w1)} implies x in N )
assume A7: x in M + {(- w1)} ; :: thesis: 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 10;
then consider u', v' being Element of V such that
A8: ( x = u' + v' & u' in M & v' in {(- w1)} ) ;
reconsider x = x as Element of V by A7;
x = u' + (- w1) by A8, TARSKI:def 1;
then x + w1 = u' + ((- w1) + w1) by RLVECT_1:def 6;
then x + w1 = u' + (0. V) by RLVECT_1:16;
then A9: x + w1 = u' by RLVECT_1:10;
u' in { (u + v) where u, v is Element of V : ( u in N & v in {w1} ) } by A1, A8, RUSUB_4:def 10;
then consider u1, v1 being Element of V such that
A10: ( u' = u1 + v1 & u1 in N & v1 in {w1} ) ;
w1 = v1 by A10, TARSKI:def 1;
hence x in N by A9, A10, RLVECT_1:21; :: thesis: verum

end;

then A11: M + {(- w1)} c= N by TARSKI:def 3;
take - w1 ; :: according to RUSUB_5:def 1 :: thesis: N = M + {(- w1)}
thus N = M + {(- w1)} by A6, A11, XBOOLE_0:def 10; :: thesis: verum