theorem :: AFF_4:64

for AS being AffinSpace
for a, b, c, d being Element of AS
for X, Y, Z being Subset of AS st X is being_plane & Y is being_plane & Z is being_plane & X '||' Y & a in X /\ Z & b in X /\ Z & c in Y /\ Z & d in Y /\ Z & X <> Y & a <> b & c <> d holds
X /\ Z // Y /\ Z