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