let k be Element of NAT ; :: thesis: for X being non empty set st 0 < k & k + 1 c= card X holds
for A being POINT of (G_ k,X)
for L being LINE of (G_ k,X) holds
( A on L iff A c= L )
let X be non empty set ; :: thesis: ( 0 < k & k + 1 c= card X implies for A being POINT of (G_ k,X)
for L being LINE of (G_ k,X) holds
( A on L iff A c= L ) )
assume A1: ( 0 < k & k + 1 c= card X ) ; :: thesis: for A being POINT of (G_ k,X)
for L being LINE of (G_ k,X) holds
( A on L iff A c= L )
then A2: the Points of (G_ k,X) = { A where A is Subset of X : card A = k } by Def1;
A3: the Lines of (G_ k,X) = { L where L is Subset of X : card L = k + 1 } by A1, Def1;
A4: the Inc of (G_ k,X) = (RelIncl (bool X)) /\ [:the Points of (G_ k,X),the Lines of (G_ k,X):] by A1, Def1;
let A be POINT of (G_ k,X); :: thesis: for L being LINE of (G_ k,X) holds
( A on L iff A c= L )
let L be LINE of (G_ k,X); :: thesis: ( A on L iff A c= L )
A in the Points of (G_ k,X) ;
then consider A1 being Subset of X such that
A5: ( A1 = A & card A1 = k ) by A2;
L in the Lines of (G_ k,X) ;
then consider L1 being Subset of X such that
A6: ( L1 = L & card L1 = k + 1 ) by A3;
thus ( A on L implies A c= L ) :: thesis: ( A c= L implies A on L )

proof

assume A on L ; :: thesis: A c= L
then [A,L] in the Inc of (G_ k,X) by INCSP_1:def 1;
then [A,L] in RelIncl (bool X) by A4, XBOOLE_0:def 4;
hence A c= L by A5, A6, WELLORD2:def 1; :: thesis: verum

end;

thus ( A c= L implies A on L ) :: thesis: verum

proof

assume A c= L ; :: thesis: A on L
then [A,L] in RelIncl (bool X) by A5, A6, WELLORD2:def 1;
then [A,L] in the Inc of (G_ k,X) by A4, XBOOLE_0:def 4;
hence A on L by INCSP_1:def 1; :: thesis: verum

end;

thus verum ; :: thesis: verum