let V be RealLinearSpace; :: thesis: for M being non empty Affine Subset of V ex L being non empty Affine Subset of V st
( L = M - M & L is Subspace-like & M is_parallel_to L )
let M be non empty Affine Subset of V; :: thesis: ex L being non empty Affine Subset of V st
( L = M - M & L is Subspace-like & M is_parallel_to L )
reconsider L = M - M as non empty Affine Subset of V by Th4, Th8;
consider v being object such that
A1: v in M by XBOOLE_0:def 1;
reconsider v = v as VECTOR of V by A1;
take L ; :: thesis: ( L = M - M & L is Subspace-like & M is_parallel_to L )
A2: 0. V in L by Th12;
( not {v} is empty & {v} is Affine ) by RUSUB_4:23;
then reconsider N = M - {v} as non empty Affine Subset of V by Th4, Th8;
A3: M is_parallel_to N
proof
take v ; :: according to RUSUB_5:def 1 :: thesis: M = N + {v}
thus M = N + {v} by Th9; :: thesis: verum
end;
N = union { (M - {u}) where u is VECTOR of V : u in M } by A1, Th19
.= L by Th18 ;
hence ( L = M - M & L is Subspace-like & M is_parallel_to L ) by A3, A2, RUSUB_4:26; :: thesis: verum