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;

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;

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

hence
N c= X
by A3; :: thesis: verumconsider 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

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

a,b // M
by A6, A16, A17, A18, A20, AFF_1:32, AFF_1:52;
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;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

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

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

hence
N c= X
by A11; :: thesis: verumassume
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;then K // N by A5, AFF_1:44;

hence N c= X by A2, A4, A9, Lm4; :: thesis: verum