let AS be AffinSpace; :: thesis: for a being Element of AS
for M, N, X being Subset of AS st X is being_plane & a in X & M c= X & a in N & ( M // N or N // M ) holds
N c= X
let a be Element of AS; :: thesis: for M, N, X being Subset of AS st X is being_plane & a in X & M c= X & a in N & ( M // N or N // M ) holds
N c= X
let M, N, X be Subset of AS; :: thesis: ( X is being_plane & a in X & M c= X & a in N & ( M // N or N // M ) implies N c= X )
assume that
A1: X is being_plane and
A2: a in X and
A3: M c= X and
A4: a in N and
A5: ( M // N or N // M ) ; :: thesis: N c= X
A6: M is being_line by A5, AFF_1:36;
consider K, P being Subset of AS such that
A7: K is being_line and
A8: P is being_line and
not K // P and
A9: X = Plane (K,P) by A1;
A10: N is being_line by A5, AFF_1:36;

A11: now :: thesis: ( not K // M implies N c= X )

assume A12: not K // M ; :: thesis: N c= X
then A13: X = Plane (K,M) by A3, A6, A7, A8, A9, Th20;
A14: a in Plane (K,M) by A2, A3, A6, A7, A8, A9, A12, Th20;

now :: thesis: ( M <> N implies N c= X )

consider a9 being Element of AS such that
A15: a,a9 // K and
A16: a9 in M by A14, Lm3;
consider b9 being Element of AS such that
A17: a9 <> b9 and
A18: b9 in M by A6, AFF_1:20;
consider b being Element of AS such that
A19: a9,a // b9,b and
A20: a9,b9 // a,b by DIRAF:40;
assume A21: M <> N ; :: thesis: N c= X
then a <> a9 by A4, A5, A16, AFF_1:45;
then b,b9 // K by A15, A19, Th4;
then A22: b in Plane (K,M) by A18;
A23: a <> b

proof

assume a = b ; :: thesis: contradiction
then a,a9 // a,b9 by A19, AFF_1:4;
then LIN a,a9,b9 by AFF_1:def 1;
then LIN a9,b9,a by AFF_1:6;
then a in M by A6, A16, A17, A18, AFF_1:25;
hence contradiction by A4, A5, A21, AFF_1:45; :: thesis: verum

end;

a,b // M by A6, A16, A17, A18, A20, AFF_1:32, AFF_1:52;
then a,b // N by A5, Th3;
then b in N by A4, Th2;
hence N c= X by A2, A4, A6, A10, A7, A13, A23, A22, Lm5; :: thesis: verum

end;

hence N c= X by A3; :: thesis: verum

end;

now :: thesis: ( K // M implies N c= X )

assume K // M ; :: thesis: N c= X
then K // N by A5, AFF_1:44;
hence N c= X by A2, A4, A9, Lm4; :: thesis: verum

end;

hence N c= X by A11; :: thesis: verum