let AS be AffinSpace; :: thesis: for X, Y being Subset of AS st X c= Y & ( ( X is being_line & Y is being_line ) or ( X is being_plane & Y is being_plane ) ) holds
X = Y
let X, Y be Subset of AS; :: thesis: ( X c= Y & ( ( X is being_line & Y is being_line ) or ( X is being_plane & Y is being_plane ) ) implies X = Y )
assume that
A1: X c= Y and
A2: ( ( X is being_line & Y is being_line ) or ( X is being_plane & Y is being_plane ) ) ; :: thesis: X = Y

A3: now :: thesis: ( X is being_plane & Y is being_plane implies X = Y )

assume that
A4: X is being_plane and
A5: Y is being_plane ; :: thesis: X = Y
consider K, P being Subset of AS such that
A6: K is being_line and
A7: P is being_line and
A8: not K // P and
A9: X = Plane (K,P) by A4;
consider a, b being Element of AS such that
A10: a in P and
b in P and
a <> b by A7, AFF_1:19;
set M = a * K;
A11: K // a * K by A6, Def3;
A12: P c= X by A6, A9, Th14;
then A13: P c= Y by A1;
A14: a * K is being_line by A6, Th27;
( a in a * K & P c= Plane (K,P) ) by A6, Def3, Th14;
then A15: a * K c= X by A9, A10, A11, Lm4;
then a * K c= Y by A1;
hence X = Y by A4, A5, A7, A8, A11, A14, A12, A13, A15, Th26; :: thesis: verum

end;

now :: thesis: ( X is being_line & Y is being_line implies X = Y )

assume that
A16: X is being_line and
A17: Y is being_line ; :: thesis: X = Y
consider a, b being Element of AS such that
A18: a <> b and
A19: X = Line (a,b) by A16, AFF_1:def 3;
( a in X & b in X ) by A19, AFF_1:15;
hence X = Y by A1, A17, A18, A19, AFF_1:57; :: thesis: verum

end;

hence X = Y by A2, A3; :: thesis: verum