let AS be AffinSpace; :: thesis: for X, Y, Z being Subset of AS st X '||' Y & Y '||' Z & Y <> {} holds

X '||' Z

let X, Y, Z be Subset of AS; :: thesis: ( X '||' Y & Y '||' Z & Y <> {} implies X '||' Z )

assume that

A1: X '||' Y and

A2: Y '||' Z and

A3: Y <> {} ; :: thesis: X '||' Z

set x = the Element of Y;

reconsider p = the Element of Y as Element of AS by A3, Lm1;

X '||' Z

let X, Y, Z be Subset of AS; :: thesis: ( X '||' Y & Y '||' Z & Y <> {} implies X '||' Z )

assume that

A1: X '||' Y and

A2: Y '||' Z and

A3: Y <> {} ; :: thesis: X '||' Z

set x = the Element of Y;

reconsider p = the Element of Y as Element of AS by A3, Lm1;

now :: thesis: for a being Element of AS

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

a * A c= Z

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

a * A c= Z

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

a * A c= Z

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

assume that

A4: a in Z and

A5: A is being_line and

A6: A c= X ; :: thesis: a * A c= Z

( p * A c= Y & p * A is being_line ) by A1, A3, A5, A6, Th27;

then a * (p * A) c= Z by A2, A4;

hence a * A c= Z by A5, Th31; :: thesis: verum

end;a * A c= Z

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

assume that

A4: a in Z and

A5: A is being_line and

A6: A c= X ; :: thesis: a * A c= Z

( p * A c= Y & p * A is being_line ) by A1, A3, A5, A6, Th27;

then a * (p * A) c= Z by A2, A4;

hence a * A c= Z by A5, Th31; :: thesis: verum