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: q + X is being_plane by Def6;
then A3: ( X '||' q + X & X '||' a + X & q + X '||' a + (q + X) & a in a + X & a in a + (q + X) & a + X is being_plane & a + (q + X) is being_plane ) by A1, Def6;
then a + X '||' q + X by A1, A2, Th61;
then a + X '||' a + (q + X) by A2, A3, Th61;
hence a + X = a + (q + X) by A3, Lm13; :: thesis: verum