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