deffunc H₁( set ) -> set = s .: $1;
consider P being Function such that
A2: ( 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 5();
A3: the Points of (G_ (k,X)) = { A where A is Subset of X : card A = k } by A1, Def1;
rng P c= the Points of (G_ (k,X))

proof

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

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in bb or y in X )
assume y in bb ; :: thesis: y in X
then ex x being object st
( x in dom s & x in A & y = s . x ) by A8, 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 bb = k by A7, A8, Th4;
hence b in the Points of (G_ (k,X)) by A3, A9; :: thesis: verum

end;

then reconsider P = P as Function of the Points of (G_ (k,X)), the Points of (G_ (k,X)) by A2, FUNCT_2:2;
A10: the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 } by A1, Def1;
consider L being Function such that
A11: ( 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 5();
rng L c= the Lines of (G_ (k,X))

proof

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

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in bb or y in X )
assume y in bb ; :: thesis: y in X
then ex x being object st
( x in dom s & x in A & y = s . x ) by A16, 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 bb = k + 1 by A15, A16, Th4;
hence b in the Lines of (G_ (k,X)) by A10, A17; :: thesis: verum

end;

then reconsider L = L as Function of the Lines of (G_ (k,X)), the Lines of (G_ (k,X)) by A11, 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 A2, A11; :: thesis: verum