let AS be AffinSpace; :: thesis: for X, Y being Subset of AS st X is being_plane & Y is being_plane holds
( X '||' Y iff ex A, P, M, N being Subset of AS st
( not A // P & A c= X & P c= X & M c= Y & N c= Y & ( A // M or M // A ) & ( P // N or N // P ) ) )
let X, Y be Subset of AS; :: thesis: ( X is being_plane & Y is being_plane implies ( X '||' Y iff ex A, P, M, N being Subset of AS st
( not A // P & A c= X & P c= X & M c= Y & N c= Y & ( A // M or M // A ) & ( P // N or N // P ) ) ) )
assume that
A1: X is being_plane and
A2: Y is being_plane ; :: thesis: ( X '||' Y iff ex A, P, M, N being Subset of AS st
( not A // P & A c= X & P c= X & M c= Y & N c= Y & ( A // M or M // A ) & ( P // N or N // P ) ) )
A3: now
given A, P, M, N being Subset of AS such that A4: not A // P and
A5: A c= X and
A6: P c= X and
A7: M c= Y and
A8: N c= Y and
A9: ( A // M or M // A ) and
A10: ( P // N or N // P ) ; :: thesis: X '||' Y
A11: M is being_line by A9, AFF_1:50;
A12: not M // N
proof
assume M // N ; :: thesis: contradiction
then P // M by A10, AFF_1:58;
hence contradiction by A4, A9, AFF_1:58; :: thesis: verum
end;
N is being_line by A10, AFF_1:50;
then consider q being Element of AS such that
A13: q in M and
A14: q in N by A2, A7, A8, A11, A12, Th22;
A15: A is being_line by A9, AFF_1:50;
A16: P is being_line by A10, AFF_1:50;
then consider p being Element of AS such that
A17: p in A and
A18: p in P by A1, A4, A5, A6, A15, Th22;
now
let a be Element of AS; :: thesis: for Z being Subset of AS st a in Y & Z is being_line & Z c= X holds
a * Z c= Y
let Z be Subset of AS; :: thesis: ( a in Y & Z is being_line & Z c= X implies a * Z c= Y )
assume that
A19: a in Y and
A20: Z is being_line and
A21: Z c= X ; :: thesis: a * Z c= Y
A22: a in a * Z by A20, Def3;
A23: Z // a * Z by A20, Def3;
A24: now
assume Z // P ; :: thesis: a * Z c= Y
then Z // N by A10, AFF_1:58;
then a * Z // N by A23, AFF_1:58;
hence a * Z c= Y by A2, A8, A19, A22, Th23; :: thesis: verum
end;
A25: now
assume that
A26: not Z // A and
A27: not Z // P ; :: thesis: a * Z c= Y
consider b being Element of AS such that
A28: p <> b and
A29: b in A by A15, AFF_1:32;
set Z1 = b * Z;
A30: b * Z is being_line by A20, Th27;
A31: not b * Z // P
proof
assume A32: b * Z // P ; :: thesis: contradiction
Z // b * Z by A20, Def3;
hence contradiction by A27, A32, AFF_1:58; :: thesis: verum
end;
A33: Z // b * Z by A20, Def3;
b * Z c= X by A1, A5, A20, A21, A29, Th28;
then consider c being Element of AS such that
A34: c in b * Z and
A35: c in P by A1, A6, A16, A30, A31, Th22;
A36: b in b * Z by A20, Def3;
then A37: p <> c by A15, A17, A26, A28, A29, A30, A33, A34, AFF_1:30;
A38: A <> P by A4, A15, AFF_1:55;
A39: not LIN p,b,c
proof
assume LIN p,b,c ; :: thesis: contradiction
then c in A by A15, A17, A28, A29, AFF_1:39;
hence contradiction by A15, A16, A17, A18, A35, A37, A38, AFF_1:30; :: thesis: verum
end;
then A40: b <> c by AFF_1:16;
consider b9 being Element of AS such that
A41: q <> b9 and
A42: b9 in M by A11, AFF_1:32;
p,b // q,b9 by A9, A17, A13, A29, A42, AFF_1:53;
then consider c9 being Element of AS such that
A43: p,c // q,c9 and
A44: b,c // b9,c9 by A41, A39, Th54;
set Z2 = Line b9,c9;
A45: ( b9 in Line b9,c9 & c9 in Line b9,c9 ) by AFF_1:26;
A46: b9 <> c9 then Line b9,c9 is being_line by AFF_1:def 3;
then b * Z // Line b9,c9 by A30, A36, A34, A44, A40, A46, A45, AFF_1:52;
then Z // Line b9,c9 by A33, AFF_1:58;
then A48: a * Z // Line b9,c9 by A23, AFF_1:58;
c9 in N by A10, A18, A14, A35, A37, A43, Th7;
then Line b9,c9 c= Y by A2, A7, A8, A42, A46, Th19;
hence a * Z c= Y by A2, A19, A22, A48, Th23; :: thesis: verum
end;
now
assume Z // A ; :: thesis: a * Z c= Y
then Z // M by A9, AFF_1:58;
then a * Z // M by A23, AFF_1:58;
hence a * Z c= Y by A2, A7, A19, A22, Th23; :: thesis: verum
end;
hence a * Z c= Y by A24, A25; :: thesis: verum
end;
hence X '||' Y by Def4; :: thesis: verum
end;
now
consider a9, b9, c9 being Element of AS such that
A49: a9 in Y and
b9 in Y and
c9 in Y and
not LIN a9,b9,c9 by A2, Th34;
assume A50: X '||' Y ; :: thesis: ex A, P being Element of K10(the carrier of AS) ex M, N being Subset of AS st
( not A // P & A c= X & P c= X & M c= Y & N c= Y & ( A // M or M // A ) & ( P // N or N // P ) )
consider a, b, c being Element of AS such that
A51: a in X and
A52: b in X and
A53: c in X and
A54: not LIN a,b,c by A1, Th34;
set A = Line a,b;
set P = Line a,c;
A55: ( b in Line a,b & c in Line a,c ) by AFF_1:26;
A56: a <> c by A54, AFF_1:16;
then A57: Line a,c c= X by A1, A51, A53, Th19;
take A = Line a,b; :: thesis: ex P being Element of K10(the carrier of AS) ex M, N being Subset of AS st
( not A // P & A c= X & P c= X & M c= Y & N c= Y & ( A // M or M // A ) & ( P // N or N // P ) )
take P = Line a,c; :: thesis: ex M, N being Subset of AS st
( not A // P & A c= X & P c= X & M c= Y & N c= Y & ( A // M or M // A ) & ( P // N or N // P ) )
take M = a9 * A; :: thesis: ex N being Subset of AS st
( not A // P & A c= X & P c= X & M c= Y & N c= Y & ( A // M or M // A ) & ( P // N or N // P ) )
take N = a9 * P; :: thesis: ( not A // P & A c= X & P c= X & M c= Y & N c= Y & ( A // M or M // A ) & ( P // N or N // P ) )
A58: a in A by AFF_1:26;
A59: a <> b by A54, AFF_1:16;
then A60: A is being_line by AFF_1:def 3;
A61: a in P by AFF_1:26;
A62: not A // P
proof
assume A // P ; :: thesis: contradiction
then A = P by A58, A61, AFF_1:59;
hence contradiction by A54, A58, A55, A60, AFF_1:33; :: thesis: verum
end;
A63: P is being_line by A56, AFF_1:def 3;
A c= X by A1, A51, A52, A59, Th19;
hence ( not A // P & A c= X & P c= X & M c= Y & N c= Y & ( A // M or M // A ) & ( P // N or N // P ) ) by A50, A60, A63, A49, A62, A57, Def3, Def4; :: thesis: verum
end;
hence ( X '||' Y iff ex A, P, M, N being Subset of AS st
( not A // P & A c= X & P c= X & M c= Y & N c= Y & ( A // M or M // A ) & ( P // N or N // P ) ) ) by A3; :: thesis: verum