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

( 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

( 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 )

( 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

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;

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

N is being_line
by A10, AFF_1:36;
assume
M // N
; :: thesis: contradiction

then P // M by A10, AFF_1:44;

hence contradiction by A4, A9, AFF_1:44; :: thesis: verum

end;then P // M by A10, AFF_1:44;

hence contradiction by A4, A9, AFF_1:44; :: thesis: verum

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

hence
X '||' Y
; :: thesis: verumfor 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;

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

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

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

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

A33:
Z // b * Z
by A20, Def3;
assume A32:
b * Z // P
; :: thesis: contradiction

Z // b * Z by A20, Def3;

hence contradiction by A27, A32, AFF_1:44; :: thesis: verum

end;Z // b * Z by A20, Def3;

hence contradiction by A27, A32, AFF_1:44; :: thesis: verum

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

then A40:
b <> c
by AFF_1:7;
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 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

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

proof

then
Line (b9,c9) is being_line
by AFF_1:def 3;
assume A47:
b9 = c9
; :: thesis: contradiction

q,b9 // M by A11, A13, A42, AFF_1:52;

then p,c // M by A41, A43, A47, Th4;

then p,c // A by A9, Th3;

then c in A by A17, Th2;

hence contradiction by A15, A16, A17, A18, A35, A37, A38, AFF_1:18; :: thesis: verum

end;q,b9 // M by A11, A13, A42, AFF_1:52;

then p,c // M by A41, A43, A47, Th4;

then p,c // A by A9, Th3;

then c in A by A17, Th2;

hence contradiction by A15, A16, A17, A18, A35, A37, A38, AFF_1:18; :: thesis: verum

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

now :: thesis: ( Z // A implies a * Z c= Y )

hence
a * Z c= Y
by A24, A25; :: thesis: verumassume
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;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

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

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

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

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

A63:
P is being_line
by A56, AFF_1:def 3;
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;then A = P by A58, A61, AFF_1:45;

hence contradiction by A54, A58, A55, A60, AFF_1:21; :: thesis: verum

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

( 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