let k be 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;

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 )

A in the Points of (G_ (k,X)) ;

then A3: ex A1 being Subset of X st

( A1 = A & card A1 = k ) by A2;

A4: the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 } by A1, Def1;

let L be LINE of (G_ (k,X)); :: thesis: ( A on L iff A c= L )

L in the Lines of (G_ (k,X)) ;

then A5: ex L1 being Subset of X st

( L1 = L & card L1 = k + 1 ) by A4;

A6: the Inc of (G_ (k,X)) = (RelIncl (bool X)) /\ [: the Points of (G_ (k,X)), the Lines of (G_ (k,X)):] by A1, Def1;

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

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;

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 )

A in the Points of (G_ (k,X)) ;

then A3: ex A1 being Subset of X st

( A1 = A & card A1 = k ) by A2;

A4: the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 } by A1, Def1;

let L be LINE of (G_ (k,X)); :: thesis: ( A on L iff A c= L )

L in the Lines of (G_ (k,X)) ;

then A5: ex L1 being Subset of X st

( L1 = L & card L1 = k + 1 ) by A4;

A6: the Inc of (G_ (k,X)) = (RelIncl (bool X)) /\ [: the Points of (G_ (k,X)), the Lines of (G_ (k,X)):] by A1, Def1;

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

proof

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

then [A,L] in the Inc of (G_ (k,X)) ;

then [A,L] in RelIncl (bool X) by A6, XBOOLE_0:def 4;

hence A c= L by A3, A5, WELLORD2:def 1; :: thesis: verum

end;then [A,L] in the Inc of (G_ (k,X)) ;

then [A,L] in RelIncl (bool X) by A6, XBOOLE_0:def 4;

hence A c= L by A3, A5, WELLORD2:def 1; :: thesis: verum