let AS be AffinSpace; :: thesis: for a being Element of AS
for X being Subset of AS st X is being_plane holds
( a in X iff a + X = X )
let a be Element of AS; :: thesis: for X being Subset of AS st X is being_plane holds
( a in X iff a + X = X )
let X be Subset of AS; :: thesis: ( X is being_plane implies ( a in X iff a + X = X ) )
assume A1: X is being_plane ; :: thesis: ( a in X iff a + X = X )

now :: thesis: ( a in X implies a + X = X )

assume A2: a in X ; :: thesis: a + X = X
X '||' X by A1, Th57;
hence a + X = X by A1, A2, Def6; :: thesis: verum

end;

hence ( a in X iff a + X = X ) by A1, Def6; :: thesis: verum