let AS be AffinSpace; :: thesis: for X, Y, Z being Subset of AS st X is being_plane & Y is being_plane & Z is being_plane & ( ( X '||' Y & Y '||' Z ) or ( X '||' Y & Z '||' Y ) or ( Y '||' X & Y '||' Z ) or ( Y '||' X & Z '||' Y ) ) holds
X '||' Z
let X, Y, Z be Subset of AS; :: thesis: ( X is being_plane & Y is being_plane & Z is being_plane & ( ( X '||' Y & Y '||' Z ) or ( X '||' Y & Z '||' Y ) or ( Y '||' X & Y '||' Z ) or ( Y '||' X & Z '||' Y ) ) implies X '||' Z )
assume that
A1: X is being_plane and
A2: Y is being_plane and
A3: ( Z is being_plane & ( ( X '||' Y & Y '||' Z ) or ( X '||' Y & Z '||' Y ) or ( Y '||' X & Y '||' Z ) or ( Y '||' X & Z '||' Y ) ) ) ; :: thesis: X '||' Z
( X '||' Y & Y '||' Z ) by A1, A2, A3, Th58;
hence X '||' Z by A2, Th59, Th60; :: thesis: verum