let AS be AffinSpace; :: thesis: for a being Element of AS

for A, X being Subset of AS st A is being_line & X is being_plane & a in A & a in X & A '||' X holds

A c= X

let a be Element of AS; :: thesis: for A, X being Subset of AS st A is being_line & X is being_plane & a in A & a in X & A '||' X holds

A c= X

let A, X be Subset of AS; :: thesis: ( A is being_line & X is being_plane & a in A & a in X & A '||' X implies A c= X )

assume that

A1: A is being_line and

A2: X is being_plane and

A3: a in A and

A4: a in X and

A5: A '||' X ; :: thesis: A c= X

consider N being Subset of AS such that

A6: N c= X and

A7: ( A // N or N // A ) by A1, A2, A5, Th41;

A8: N is being_line by A7, AFF_1:36;

A = a * A by A1, A3, Lm8

.= a * N by A7, Th32 ;

hence A c= X by A2, A4, A6, A8, Th28; :: thesis: verum

for A, X being Subset of AS st A is being_line & X is being_plane & a in A & a in X & A '||' X holds

A c= X

let a be Element of AS; :: thesis: for A, X being Subset of AS st A is being_line & X is being_plane & a in A & a in X & A '||' X holds

A c= X

let A, X be Subset of AS; :: thesis: ( A is being_line & X is being_plane & a in A & a in X & A '||' X implies A c= X )

assume that

A1: A is being_line and

A2: X is being_plane and

A3: a in A and

A4: a in X and

A5: A '||' X ; :: thesis: A c= X

consider N being Subset of AS such that

A6: N c= X and

A7: ( A // N or N // A ) by A1, A2, A5, Th41;

A8: N is being_line by A7, AFF_1:36;

A = a * A by A1, A3, Lm8

.= a * N by A7, Th32 ;

hence A c= X by A2, A4, A6, A8, Th28; :: thesis: verum