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

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;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

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

hence
X = Y
by A2, A3; :: thesis: verumassume 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;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