deffunc H₁( set ) -> set = s .: $1;
consider P being Function such that
A1: ( dom P = the Points of (G_ (k,X)) & ( for x being set st x in the Points of (G_ (k,X)) holds
P . x = H₁(x) ) ) from FUNCT_1:sch 3();
A2: the Points of (G_ (k,X)) = { A where A is Subset of X : card A = k } by B1, Def1;
rng P c= the Points of (G_ (k,X))

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in rng P or b in the Points of (G_ (k,X)) )
assume b in rng P ; :: thesis: b in the Points of (G_ (k,X))
then consider a being set such that
A3: a in the Points of (G_ (k,X)) and
A4: b = P . a by A1, FUNCT_1:def 3;
consider A being Subset of X such that
A5: A = a and
A6: card A = k by A2, A3;
A7: b = s .: A by A1, A3, A4, A5;
A8: b c= X

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in b or y in X )
assume y in b ; :: thesis: y in X
then ex x being set st
( x in dom s & x in A & y = s . x ) by A7, FUNCT_1:def 6;
then y in rng s by FUNCT_1:3;
hence y in X by FUNCT_2:def 3; :: thesis: verum

end;

dom s = X by FUNCT_2:def 1;
then card b = k by A6, A7, Th4;
hence b in the Points of (G_ (k,X)) by A2, A8; :: thesis: verum

end;

then reconsider P = P as Function of the Points of (G_ (k,X)), the Points of (G_ (k,X)) by A1, FUNCT_2:2;
A9: the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 } by B1, Def1;
consider L being Function such that
A10: ( dom L = the Lines of (G_ (k,X)) & ( for x being set st x in the Lines of (G_ (k,X)) holds
L . x = H₁(x) ) ) from FUNCT_1:sch 3();
rng L c= the Lines of (G_ (k,X))

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in rng L or b in the Lines of (G_ (k,X)) )
assume b in rng L ; :: thesis: b in the Lines of (G_ (k,X))
then consider a being set such that
A11: a in the Lines of (G_ (k,X)) and
A12: b = L . a by A10, FUNCT_1:def 3;
consider A being Subset of X such that
A13: A = a and
A14: card A = k + 1 by A9, A11;
A15: b = s .: A by A10, A11, A12, A13;
A16: b c= X

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in b or y in X )
assume y in b ; :: thesis: y in X
then ex x being set st
( x in dom s & x in A & y = s . x ) by A15, FUNCT_1:def 6;
then y in rng s by FUNCT_1:3;
hence y in X by FUNCT_2:def 3; :: thesis: verum

end;

dom s = X by FUNCT_2:def 1;
then card b = k + 1 by A14, A15, Th4;
hence b in the Lines of (G_ (k,X)) by A9, A16; :: thesis: verum

end;

then reconsider L = L as Function of the Lines of (G_ (k,X)), the Lines of (G_ (k,X)) by A10, FUNCT_2:2;
take IncProjMap(# P,L #) ; :: thesis: ( ( for A being POINT of (G_ (k,X)) holds IncProjMap(# P,L #) . A = s .: A ) & ( for L being LINE of (G_ (k,X)) holds IncProjMap(# P,L #) . L = s .: L ) )
thus ( ( for A being POINT of (G_ (k,X)) holds IncProjMap(# P,L #) . A = s .: A ) & ( for L being LINE of (G_ (k,X)) holds IncProjMap(# P,L #) . L = s .: L ) ) by A1, A10; :: thesis: verum