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 and

A2: Y is being_plane and

A3: X '||' Y ; :: thesis: a + X = a + Y

A4: a + X is being_plane by A1, Def6;

A5: ( a in a + X & a in a + Y ) by A1, A2, Def6;

A6: a + Y is being_plane by A2, Def6;

X '||' a + X by A1, Def6;

then A7: a + X '||' Y by A1, A2, A3, A4, Th61;

Y '||' a + Y by A2, Def6;

then a + X '||' a + Y by A2, A4, A6, A7, Th61;

hence a + X = a + Y by A5, A4, A6, Lm13; :: thesis: verum

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 and

A2: Y is being_plane and

A3: X '||' Y ; :: thesis: a + X = a + Y

A4: a + X is being_plane by A1, Def6;

A5: ( a in a + X & a in a + Y ) by A1, A2, Def6;

A6: a + Y is being_plane by A2, Def6;

X '||' a + X by A1, Def6;

then A7: a + X '||' Y by A1, A2, A3, A4, Th61;

Y '||' a + Y by A2, Def6;

then a + X '||' a + Y by A2, A4, A6, A7, Th61;

hence a + X = a + Y by A5, A4, A6, Lm13; :: thesis: verum