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

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