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;
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
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;
hence X '||' Z ; :: thesis: verum