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 A1: ( X is being_plane & 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 ) ) )

A2: now

assume A3: 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
A4: ( a in X & b in X & c in X ) and
A5: not LIN a,b,c by A1, Th34;
A6: ( a <> b & a <> c & b <> c ) by A5, AFF_1:16;
set A = Line a,b;
set P = Line a,c;
A7: ( a in Line a,b & b in Line a,b & a in Line a,c & c in Line a,c & Line a,b is being_line & Line a,c is being_line ) by A6, AFF_1:26, AFF_1:def 3;
consider a', b', c' being Element of AS such that
A8: a' in Y and
( b' in Y & c' in Y & not LIN a',b',c' ) by A1, Th34;
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 = a' * 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 = a' * 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 ) )
A9: not A // P

proof

assume A // P ; :: thesis: contradiction
then A = P by A7, AFF_1:59;
hence contradiction by A5, A7, AFF_1:33; :: thesis: verum

end;

( A c= X & P c= X ) by A1, A4, A6, 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 A3, A7, A8, A9, Def3, Def4; :: thesis: verum

end;

now

given A, P, M, N being Subset of AS such that A10: not A // P and
A11: ( A c= X & P c= X & M c= Y & N c= Y ) and
A12: ( A // M or M // A ) and
A13: ( P // N or N // P ) ; :: thesis: X '||' Y
A14: ( A is being_line & P is being_line & M is being_line & N is being_line ) by A12, A13, AFF_1:50;
then consider p being Element of AS such that
A15: ( p in A & p in P ) by A1, A10, A11, Th22;
not M // N

proof

assume M // N ; :: thesis: contradiction
then P // M by A13, AFF_1:58;
hence contradiction by A10, A12, AFF_1:58; :: thesis: verum

end;

then consider q being Element of AS such that
A16: ( q in M & q in N ) by A1, A11, A14, 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 A17: ( a in Y & Z is being_line & Z c= X ) ; :: thesis: a * Z c= Y
then A18: ( Z // a * Z & a in a * Z ) by Def3;

A19: now

assume Z // A ; :: thesis: a * Z c= Y
then Z // M by A12, AFF_1:58;
then a * Z // M by A18, AFF_1:58;
hence a * Z c= Y by A1, A11, A17, A18, Th23; :: thesis: verum

end;

A20: now

assume Z // P ; :: thesis: a * Z c= Y
then Z // N by A13, AFF_1:58;
then a * Z // N by A18, AFF_1:58;
hence a * Z c= Y by A1, A11, A17, A18, Th23; :: thesis: verum

end;

now

assume A21: ( not Z // A & not Z // P ) ; :: thesis: a * Z c= Y
consider b being Element of AS such that
A22: ( p <> b & b in A ) by A14, AFF_1:32;
set Z1 = b * Z;
A23: ( b * Z is being_line & b in b * Z & Z // b * Z ) by A17, Def3, Th27;
A24: not b * Z // P

proof

assume b * Z // P ; :: thesis: contradiction
then ( b * Z // P & Z // b * Z ) by A17, Def3;
hence contradiction by A21, AFF_1:58; :: thesis: verum

end;

b * Z c= X by A1, A11, A17, A22, Th28;
then consider c being Element of AS such that
A25: ( c in b * Z & c in P ) by A1, A11, A14, A23, A24, Th22;
A26: p <> c by A14, A15, A21, A22, A23, A25, AFF_1:30;
consider b' being Element of AS such that
A27: ( q <> b' & b' in M ) by A14, AFF_1:32;
A28: p,b // q,b' by A12, A15, A16, A22, A27, AFF_1:53;
A29: A <> P by A10, A14, AFF_1:55;
A30: not LIN p,b,c

proof

assume LIN p,b,c ; :: thesis: contradiction
then c in A by A14, A15, A22, AFF_1:39;
hence contradiction by A14, A15, A25, A26, A29, AFF_1:30; :: thesis: verum

end;

then consider c' being Element of AS such that
A31: ( p,c // q,c' & b,c // b',c' ) by A27, A28, Th54;
A32: ( b <> c & p <> b ) by A30, AFF_1:16;
A33: c' in N by A13, A15, A16, A25, A26, A31, Th7;
set Z2 = Line b',c';
A34: b' <> c'

proof

assume b' = c' ; :: thesis: contradiction
then ( p,c // q,b' & q,b' // M ) by A14, A16, A27, A31, AFF_1:66;
then p,c // M by A27, Th4;
then p,c // A by A12, Th3;
then c in A by A15, Th2;
hence contradiction by A14, A15, A25, A26, A29, AFF_1:30; :: thesis: verum

end;

then ( Line b',c' is being_line & b' in Line b',c' & c' in Line b',c' ) by AFF_1:26, AFF_1:def 3;
then b * Z // Line b',c' by A23, A25, A31, A32, A34, AFF_1:52;
then A35: Z // Line b',c' by A23, AFF_1:58;
A36: Line b',c' c= Y by A1, A11, A27, A33, A34, Th19;
a * Z // Line b',c' by A18, A35, AFF_1:58;
hence a * Z c= Y by A1, A17, A18, A36, Th23; :: thesis: verum

end;

hence a * Z c= Y by A19, A20; :: thesis: verum

end;

hence X '||' Y by 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 A2; :: thesis: verum