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 )

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 )

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

X '||' X by A1, Th57;

hence a + X = X by A1, A2, Def6; :: thesis: verum

end;X '||' X by A1, Th57;

hence a + X = X by A1, A2, Def6; :: thesis: verum