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 :: thesis: ( 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 ) ) implies X '||' Y )
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:36;
A12: not M // N
proof
assume M // N ; :: thesis: contradiction
then P // M by A10, AFF_1:44;
hence contradiction by A4, A9, AFF_1:44; :: thesis: verum
end;
N is being_line by A10, AFF_1:36;
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:36;
A16: P is being_line by A10, AFF_1:36;
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 :: thesis: for a being Element of AS
for Z being Subset of AS st a in Y & Z is being_line & Z c= X holds
a * Z c= Y
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 :: thesis: ( Z // P implies a * Z c= Y )
assume Z // P ; :: thesis: a * Z c= Y
then Z // N by A10, AFF_1:44;
then a * Z // N by A23, AFF_1:44;
hence a * Z c= Y by A2, A8, A19, A22, Th23; :: thesis: verum
end;
A25: now :: thesis: ( not Z // A & not Z // P implies a * Z c= Y )
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:20;
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:44; :: 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:18;
A38: A <> P by A4, A15, AFF_1:41;
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:25;
hence contradiction by A15, A16, A17, A18, A35, A37, A38, AFF_1:18; :: thesis: verum
end;
then A40: b <> c by AFF_1:7;
consider b9 being Element of AS such that
A41: q <> b9 and
A42: b9 in M by A11, AFF_1:20;
p,b // q,b9 by A9, A17, A13, A29, A42, AFF_1:39;
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:15;
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:38;
then Z // Line (b9,c9) by A33, AFF_1:44;
then A48: a * Z // Line (b9,c9) by A23, AFF_1:44;
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 :: thesis: ( Z // A implies a * Z c= Y )
assume Z // A ; :: thesis: a * Z c= Y
then Z // M by A9, AFF_1:44;
then a * Z // M by A23, AFF_1:44;
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 ; :: thesis: verum
end;
now :: thesis: ( X '||' Y implies ex A, P being Element of K24( 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 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 K24( 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:15;
A56: a <> c by A54, AFF_1:7;
then A57: Line (a,c) c= X by A1, A51, A53, Th19;
take A = Line (a,b); :: thesis: ex P being Element of K24( 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:15;
A59: a <> b by A54, AFF_1:7;
then A60: A is being_line by AFF_1:def 3;
A61: a in P by AFF_1:15;
A62: not A // P
proof
assume A // P ; :: thesis: contradiction
then A = P by A58, A61, AFF_1:45;
hence contradiction by A54, A58, A55, A60, AFF_1:21; :: 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; :: 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