let AS be AffinSpace; :: thesis: for x being Element of AS
for X, X', Y, Y' being Subset of AS
for p, b, c being POINT of (IncProjSp_of AS)
for A, K, M being LINE of (IncProjSp_of AS) st X is being_line & X' is being_line & Y is being_plane & X c= Y & X' c= Y & x = p & A = [X,1] & K = [X',1] & A <> K & b on A & c on K & b on M & c on M & b <> c & M = [Y',1] & Y' is being_line holds
Y' c= Y
let x be Element of AS; :: thesis: for X, X', Y, Y' being Subset of AS
for p, b, c being POINT of (IncProjSp_of AS)
for A, K, M being LINE of (IncProjSp_of AS) st X is being_line & X' is being_line & Y is being_plane & X c= Y & X' c= Y & x = p & A = [X,1] & K = [X',1] & A <> K & b on A & c on K & b on M & c on M & b <> c & M = [Y',1] & Y' is being_line holds
Y' c= Y
let X, X', Y, Y' be Subset of AS; :: thesis: for p, b, c being POINT of (IncProjSp_of AS)
for A, K, M being LINE of (IncProjSp_of AS) st X is being_line & X' is being_line & Y is being_plane & X c= Y & X' c= Y & x = p & A = [X,1] & K = [X',1] & A <> K & b on A & c on K & b on M & c on M & b <> c & M = [Y',1] & Y' is being_line holds
Y' c= Y
let p, b, c be POINT of (IncProjSp_of AS); :: thesis: for A, K, M being LINE of (IncProjSp_of AS) st X is being_line & X' is being_line & Y is being_plane & X c= Y & X' c= Y & x = p & A = [X,1] & K = [X',1] & A <> K & b on A & c on K & b on M & c on M & b <> c & M = [Y',1] & Y' is being_line holds
Y' c= Y
let A, K, M be LINE of (IncProjSp_of AS); :: thesis: ( X is being_line & X' is being_line & Y is being_plane & X c= Y & X' c= Y & x = p & A = [X,1] & K = [X',1] & A <> K & b on A & c on K & b on M & c on M & b <> c & M = [Y',1] & Y' is being_line implies Y' c= Y )
assume that
A1:
( X is being_line & X' is being_line & Y is being_plane )
and
A2:
( X c= Y & X' c= Y )
and
A3:
( x = p & A = [X,1] & K = [X',1] & A <> K )
and
A4:
( b on A & c on K & b on M & c on M & b <> c )
and
A5:
( M = [Y',1] & Y' is being_line )
; :: thesis: Y' c= Y
A6:
now assume
b is
Element of
AS
;
:: thesis: Y' c= Ythen reconsider y =
b as
Element of
AS ;
A7:
now assume
c is
Element of
AS
;
:: thesis: Y' c= Ythen reconsider z =
c as
Element of
AS ;
A8:
(
y in Y' &
z in Y' )
by A4, A5, Th26;
A9:
(
y in X &
z in X' )
by A3, A4, Th26;
Y' = Line y,
z
by A4, A5, A8, AFF_1:71;
hence
Y' c= Y
by A1, A2, A4, A9, AFF_4:19;
:: thesis: verum end; now given Xc being
Subset of
AS such that A10:
(
c = LDir Xc &
Xc is
being_line )
;
:: thesis: Y' c= YA11:
(
y in Y' &
y in X )
by A3, A4, A5, Th26;
Xc '||' Y'
by A4, A5, A10, Th28;
then A12:
Xc // Y'
by A5, A10, AFF_4:40;
Xc '||' X'
by A1, A3, A4, A10, Th28;
then
Xc // X'
by A1, A10, AFF_4:40;
then
X' // Y'
by A12, AFF_1:58;
then
Y' = y * X'
by A1, A11, AFF_4:def 3;
hence
Y' c= Y
by A1, A2, A11, AFF_4:28;
:: thesis: verum end; hence
Y' c= Y
by A7, Th20;
:: thesis: verum end;
now given Xb being
Subset of
AS such that A13:
(
b = LDir Xb &
Xb is
being_line )
;
:: thesis: Y' c= YA14:
now assume
c is
Element of
AS
;
:: thesis: Y' c= Ythen reconsider y =
c as
Element of
AS ;
A15:
(
y in Y' &
y in X' )
by A3, A4, A5, Th26;
Xb '||' Y'
by A4, A5, A13, Th28;
then A16:
Xb // Y'
by A5, A13, AFF_4:40;
Xb '||' X
by A1, A3, A4, A13, Th28;
then
Xb // X
by A1, A13, AFF_4:40;
then
X // Y'
by A16, AFF_1:58;
then
Y' = y * X
by A1, A15, AFF_4:def 3;
hence
Y' c= Y
by A1, A2, A15, AFF_4:28;
:: thesis: verum end; now given Xc being
Subset of
AS such that A17:
(
c = LDir Xc &
Xc is
being_line )
;
:: thesis: contradiction
(
Xc '||' Y' &
Xb '||' Y' )
by A4, A5, A13, A17, Th28;
then
(
Xc // Y' &
Xb // Y' )
by A5, A13, A17, AFF_4:40;
then
Xc // Xb
by AFF_1:58;
hence
contradiction
by A4, A13, A17, Th11;
:: thesis: verum end; hence
Y' c= Y
by A14, Th20;
:: thesis: verum end;
hence
Y' c= Y
by A6, Th20; :: thesis: verum