let AS be AffinSpace; :: thesis: for X, Y, X9, Y9 being Subset of AS
for b, c being POINT of (IncProjSp_of AS)
for A, K, M being LINE of (IncProjSp_of AS) st X is being_line & X9 is being_line & Y is being_plane & X c= Y & X9 c= Y & A = [X,1] & K = [X9,1] & b on A & c on K & b on M & c on M & b <> c & M = [Y9,1] & Y9 is being_line holds
Y9 c= Y
let X, Y, X9, Y9 be Subset of AS; :: thesis: for b, c being POINT of (IncProjSp_of AS)
for A, K, M being LINE of (IncProjSp_of AS) st X is being_line & X9 is being_line & Y is being_plane & X c= Y & X9 c= Y & A = [X,1] & K = [X9,1] & b on A & c on K & b on M & c on M & b <> c & M = [Y9,1] & Y9 is being_line holds
Y9 c= Y
let b, c be POINT of (IncProjSp_of AS); :: thesis: for A, K, M being LINE of (IncProjSp_of AS) st X is being_line & X9 is being_line & Y is being_plane & X c= Y & X9 c= Y & A = [X,1] & K = [X9,1] & b on A & c on K & b on M & c on M & b <> c & M = [Y9,1] & Y9 is being_line holds
Y9 c= Y
let A, K, M be LINE of (IncProjSp_of AS); :: thesis: ( X is being_line & X9 is being_line & Y is being_plane & X c= Y & X9 c= Y & A = [X,1] & K = [X9,1] & b on A & c on K & b on M & c on M & b <> c & M = [Y9,1] & Y9 is being_line implies Y9 c= Y )
assume that
A1: X is being_line and
A2: X9 is being_line and
A3: Y is being_plane and
A4: X c= Y and
A5: X9 c= Y and
A6: A = [X,1] and
A7: K = [X9,1] and
A8: b on A and
A9: c on K and
A10: b on M and
A11: c on M and
A12: b <> c and
A13: M = [Y9,1] and
A14: Y9 is being_line ; :: thesis: Y9 c= Y

A15: now :: thesis: ( b is Element of AS implies Y9 c= Y )

assume b is Element of AS ; :: thesis: Y9 c= Y
then reconsider y = b as Element of AS ;

A16: now :: thesis: ( ex Xc being Subset of AS st
( c = LDir Xc & Xc is being_line ) implies Y9 c= Y )

given Xc being Subset of AS such that A17: c = LDir Xc and
A18: Xc is being_line ; :: thesis: Y9 c= Y
Xc '||' X9 by A2, A7, A9, A17, A18, Th28;
then A19: Xc // X9 by A2, A18, AFF_4:40;
Xc '||' Y9 by A11, A13, A14, A17, A18, Th28;
then Xc // Y9 by A14, A18, AFF_4:40;
then A20: X9 // Y9 by A19, AFF_1:44;
y in Y9 by A10, A13, Th26;
then A21: Y9 = y * X9 by A2, A20, AFF_4:def 3;
y in X by A6, A8, Th26;
hence Y9 c= Y by A2, A3, A4, A5, A21, AFF_4:28; :: thesis: verum

end;

now :: thesis: ( c is Element of AS implies Y9 c= Y )

assume c is Element of AS ; :: thesis: Y9 c= Y
then reconsider z = c as Element of AS ;
A22: z in Y9 by A11, A13, Th26;
y in Y9 by A10, A13, Th26;
then A23: Y9 = Line (y,z) by A12, A14, A22, AFF_1:57;
A24: z in X9 by A7, A9, Th26;
y in X by A6, A8, Th26;
hence Y9 c= Y by A3, A4, A5, A12, A24, A23, AFF_4:19; :: thesis: verum

end;

hence Y9 c= Y by A16, Th20; :: thesis: verum

end;

now :: thesis: ( ex Xb being Subset of AS st
( b = LDir Xb & Xb is being_line ) implies Y9 c= Y )

given Xb being Subset of AS such that A25: b = LDir Xb and
A26: Xb is being_line ; :: thesis: Y9 c= Y

A27: now :: thesis: ( c is Element of AS implies Y9 c= Y )

assume c is Element of AS ; :: thesis: Y9 c= Y
then reconsider y = c as Element of AS ;
Xb '||' X by A1, A6, A8, A25, A26, Th28;
then A28: Xb // X by A1, A26, AFF_4:40;
Xb '||' Y9 by A10, A13, A14, A25, A26, Th28;
then Xb // Y9 by A14, A26, AFF_4:40;
then A29: X // Y9 by A28, AFF_1:44;
y in Y9 by A11, A13, Th26;
then A30: Y9 = y * X by A1, A29, AFF_4:def 3;
y in X9 by A7, A9, Th26;
hence Y9 c= Y by A1, A3, A4, A5, A30, AFF_4:28; :: thesis: verum

end;

now :: thesis: for Xc being Subset of AS holds
( not c = LDir Xc or not Xc is being_line )

Xb '||' Y9 by A10, A13, A14, A25, A26, Th28;
then A31: Xb // Y9 by A14, A26, AFF_4:40;
given Xc being Subset of AS such that A32: c = LDir Xc and
A33: Xc is being_line ; :: thesis: contradiction
Xc '||' Y9 by A11, A13, A14, A32, A33, Th28;
then Xc // Y9 by A14, A33, AFF_4:40;
then Xc // Xb by A31, AFF_1:44;
hence contradiction by A12, A25, A26, A32, A33, Th11; :: thesis: verum

end;

hence Y9 c= Y by A27, Th20; :: thesis: verum

end;

hence Y9 c= Y by A15, Th20; :: thesis: verum