let AS be AffinSpace; :: thesis: for A, M, X being Subset of AS st A // M & M '||' X holds

A '||' X

let A, M, X be Subset of AS; :: thesis: ( A // M & M '||' X implies A '||' X )

assume that

A1: A // M and

A2: M '||' X ; :: thesis: A '||' X

A3: M is being_line by A1, AFF_1:36;

A4: A is being_line by A1, AFF_1:36;

A '||' X

let A, M, X be Subset of AS; :: thesis: ( A // M & M '||' X implies A '||' X )

assume that

A1: A // M and

A2: M '||' X ; :: thesis: A '||' X

A3: M is being_line by A1, AFF_1:36;

A4: A is being_line by A1, AFF_1:36;

now :: thesis: for a being Element of AS

for C being Subset of AS st a in X & C is being_line & C c= A holds

a * C c= X

hence
A '||' X
; :: thesis: verumfor C being Subset of AS st a in X & C is being_line & C c= A holds

a * C c= X

consider q, p being Element of AS such that

A5: q in A and

p in A and

q <> p by A4, AFF_1:19;

let a be Element of AS; :: thesis: for C being Subset of AS st a in X & C is being_line & C c= A holds

a * C c= X

let C be Subset of AS; :: thesis: ( a in X & C is being_line & C c= A implies a * C c= X )

assume that

A6: a in X and

A7: ( C is being_line & C c= A ) ; :: thesis: a * C c= X

A8: a * A = a * (q * M) by A1, A3, A5, Def3

.= a * M by A3, Th31 ;

C = A by A4, A7, Th33;

hence a * C c= X by A2, A3, A6, A8; :: thesis: verum

end;A5: q in A and

p in A and

q <> p by A4, AFF_1:19;

let a be Element of AS; :: thesis: for C being Subset of AS st a in X & C is being_line & C c= A holds

a * C c= X

let C be Subset of AS; :: thesis: ( a in X & C is being_line & C c= A implies a * C c= X )

assume that

A6: a in X and

A7: ( C is being_line & C c= A ) ; :: thesis: a * C c= X

A8: a * A = a * (q * M) by A1, A3, A5, Def3

.= a * M by A3, Th31 ;

C = A by A4, A7, Th33;

hence a * C c= X by A2, A3, A6, A8; :: thesis: verum