let AS be AffinSpace; ( AS is AffinPlane implies AfLines AS misses Dir_of_Planes AS )
the carrier of AS c= the carrier of AS
;
then reconsider X9 = the carrier of AS as Subset of AS ;
assume
AS is AffinPlane
; AfLines AS misses Dir_of_Planes AS
then A1:
X9 is being_plane
by Th1;
assume
not AfLines AS misses Dir_of_Planes AS
; contradiction
then consider x being object such that
A2:
x in AfLines AS
and
A3:
x in Dir_of_Planes AS
by XBOOLE_0:3;
consider Y being Subset of AS such that
A4:
x = Y
and
A5:
Y is being_line
by A2;
consider X being Subset of AS such that
A6:
x = PDir X
and
A7:
X is being_plane
by A3, Th15;
consider a, b being Element of AS such that
A8:
a in Y
and
b in Y
and
a <> b
by A5, AFF_1:19;
consider Y9 being Subset of AS such that
A9:
a = Y9
and
A10:
Y9 is being_plane
and
X '||' Y9
by A6, A7, A4, A8, Th10;
A11:
not Y9 in Y9
;
Y9 = X9
by A1, A10, AFF_4:33;
hence
contradiction
by A9, A11; verum