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} ;
set w2 = - w1;
for x being object st x in N holds
x in M + {(- w1)}

proof

let x be object ; :: 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 ;
set y = x + w1;
w1 in {w1} by TARSKI:def 1;
then x + w1 in { (u + v) where u, v is Element of V : ( u in N & v in {w1} ) } by A2;
then A3: x + w1 in M by A1, RUSUB_4:def 9;
x + (w1 + (- w1)) = (x + w1) + (- w1) by RLVECT_1:def 3;
then x + (0. V) = (x + w1) + (- w1) by RLVECT_1:5;
then A4: x = (x + w1) + (- w1) ;
- 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 A3, A4;
hence x in M + {(- w1)} by RUSUB_4:def 9; :: thesis: verum

end;

then A5: N c= M + {(- w1)} ;
take - w1 ; :: according to RUSUB_5:def 1 :: thesis: N = M + {(- w1)}
for x being object st x in M + {(- w1)} holds
x in N

proof

let x be object ; :: thesis: ( x in M + {(- w1)} implies x in N )
assume A6: 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 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; :: thesis: verum

end;

then M + {(- w1)} c= N ;
hence N = M + {(- w1)} by A5; :: thesis: verum