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 )
proof
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;
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 A3, A5, WELLORD2:def 1;
then [A,L] in the Inc of (G_ (k,X)) by A6, XBOOLE_0:def 4;
hence A on L ; :: thesis: verum
end;