let V be non empty right_zeroed RLSStruct ; :: thesis: for M being Affine Subset of V holds M is_parallel_to M
let M be Affine Subset of V; :: thesis: M is_parallel_to M
take 0. V ; :: according to RUSUB_5:def 1 :: thesis: M = M + {(0. V)}
for x being object st x in M + {(0. V)} holds
x in M

proof

let x be object ; :: thesis: ( x in M + {(0. V)} implies x in M )
assume x in M + {(0. V)} ; :: thesis: x in M
then x in { (u + v) where u, v is Element of V : ( u in M & v in {(0. V)} ) } by RUSUB_4:def 9;
then consider u, v being Element of V such that
A1: ( x = u + v & u in M ) and
A2: v in {(0. V)} ;
v = 0. V by A2, TARSKI:def 1;
hence x in M by A1, RLVECT_1:def 4; :: thesis: verum

end;

then A3: M + {(0. V)} c= M ;
for x being object st x in M holds
x in M + {(0. V)}

proof

let x be object ; :: thesis: ( x in M implies x in M + {(0. V)} )
assume A4: x in M ; :: thesis: x in M + {(0. V)}
then reconsider x = x as Element of V ;
( x = x + (0. V) & 0. V in {(0. V)} ) by RLVECT_1:def 4, TARSKI:def 1;
then x in { (u + v) where u, v is Element of V : ( u in M & v in {(0. V)} ) } by A4;
hence x in M + {(0. V)} by RUSUB_4:def 9; :: thesis: verum

end;

then M c= M + {(0. V)} ;
hence M = M + {(0. V)} by A3; :: thesis: verum