let AS be AffinSpace; :: thesis: for X, X', Y, Y' being Subset of
for b, c being POINT of
for A, K, M being LINE of st X is being_line & X' is being_line & Y is being_plane & X c= Y & X' c= Y & A = [X,1] & K = [X',1] & b on A & c on K & b on M & c on M & b <> c & M = [(PDir Y'),2] & Y' is being_plane holds
( Y' '||' Y & Y '||' Y' )
let X, X', Y, Y' be Subset of ; :: thesis: for b, c being POINT of
for A, K, M being LINE of st X is being_line & X' is being_line & Y is being_plane & X c= Y & X' c= Y & A = [X,1] & K = [X',1] & b on A & c on K & b on M & c on M & b <> c & M = [(PDir Y'),2] & Y' is being_plane holds
( Y' '||' Y & Y '||' Y' )
let b, c be POINT of ; :: thesis: for A, K, M being LINE of st X is being_line & X' is being_line & Y is being_plane & X c= Y & X' c= Y & A = [X,1] & K = [X',1] & b on A & c on K & b on M & c on M & b <> c & M = [(PDir Y'),2] & Y' is being_plane holds
( Y' '||' Y & Y '||' Y' )
let A, K, M be LINE of ; :: thesis: ( X is being_line & X' is being_line & Y is being_plane & X c= Y & X' c= Y & A = [X,1] & K = [X',1] & b on A & c on K & b on M & c on M & b <> c & M = [(PDir Y'),2] & Y' is being_plane implies ( Y' '||' Y & Y '||' Y' ) )
assume that
A1: X is being_line and
A2: X' is being_line and
A3: Y is being_plane and
A4: X c= Y and
A5: X' c= Y and
A6: A = [X,1] and
A7: K = [X',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 = [(PDir Y'),2] and
A14: Y' is being_plane ; :: thesis: ( Y' '||' Y & Y '||' Y' )
( b is Element of or ex Xb being Subset of st
( b = LDir Xb & Xb is being_line ) ) by Th20;
then consider Xb being Subset of such that
A15: b = LDir Xb and
A16: Xb is being_line by A10, A13, Th27;
A17: Xb '||' Y' by A10, A13, A14, A15, A16, Th29;
Xb '||' X by A1, A6, A8, A15, A16, Th28;
then Xb // X by A1, A16, AFF_4:40;
then A18: Xb '||' Y by A1, A3, A4, AFF_4:42, AFF_4:56;
( c is Element of or ex Xc being Subset of st
( c = LDir Xc & Xc is being_line ) ) by Th20;
then consider Xc being Subset of such that
A19: c = LDir Xc and
A20: Xc is being_line by A11, A13, Th27;
A21: Xc '||' Y' by A11, A13, A14, A19, A20, Th29;
Xc '||' X' by A2, A7, A9, A19, A20, Th28;
then Xc // X' by A2, A20, AFF_4:40;
then A22: Xc '||' Y by A2, A3, A5, AFF_4:42, AFF_4:56;
not Xb // Xc by A12, A15, A16, A19, A20, Th11;
hence ( Y' '||' Y & Y '||' Y' ) by A3, A14, A16, A20, A17, A21, A18, A22, Th5; :: thesis: verum