let AS be AffinSpace; :: thesis: for a, q being Element of AS
for X being Subset of AS st X is being_plane holds
a + X = a + (q + X)
let a, q be Element of AS; :: thesis: for X being Subset of AS st X is being_plane holds
a + X = a + (q + X)
let X be Subset of AS; :: thesis: ( X is being_plane implies a + X = a + (q + X) )
assume A1: X is being_plane ; :: thesis: a + X = a + (q + X)
then A2: a in a + X by Def6;
A3: a + X is being_plane by A1, Def6;
A4: q + X is being_plane by A1, Def6;
then A5: q + X '||' a + (q + X) by Def6;
A6: a in a + (q + X) by A4, Def6;
A7: a + (q + X) is being_plane by A4, Def6;
( X '||' q + X & X '||' a + X ) by A1, Def6;
then a + X '||' q + X by A1, A4, A3, Th61;
then a + X '||' a + (q + X) by A4, A5, A3, A7, Th61;
hence a + X = a + (q + X) by A2, A6, A3, A7, Lm13; :: thesis: verum