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 X' = the carrier of AS as Subset of ;
assume
AS is AffinPlane
; AfLines AS misses Dir_of_Planes AS
then A1:
X' is being_plane
by Th1;
assume
not AfLines AS misses Dir_of_Planes AS
; contradiction
then consider x being set such that
A2:
x in AfLines AS
and
A3:
x in Dir_of_Planes AS
by XBOOLE_0:3;
consider Y being Subset of such that
A4:
x = Y
and
A5:
Y is being_line
by A2;
consider X being Subset of such that
A6:
x = PDir X
and
A7:
X is being_plane
by A3, Th15;
consider a, b being Element of such that
A8:
a in Y
and
b in Y
and
a <> b
by A5, AFF_1:31;
consider Y' being Subset of such that
A9:
a = Y'
and
A10:
Y' is being_plane
and
X '||' Y'
by A6, A7, A4, A8, Th10;
A11:
not Y' in Y'
;
Y' = X'
by A1, A10, AFF_4:33;
hence
contradiction
by A9, A11; verum