let k be Element of NAT ; :: thesis: for X being non empty set st 0 < k & k + 1 c= card X holds

for T being Subset of the Points of (G_ (k,X)) st T is STAR holds

for S being Subset of X st S = meet T holds

( card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } )

let X be non empty set ; :: thesis: ( 0 < k & k + 1 c= card X implies for T being Subset of the Points of (G_ (k,X)) st T is STAR holds

for S being Subset of X st S = meet T holds

( card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } ) )

assume A1: ( 0 < k & k + 1 c= card X ) ; :: thesis: for T being Subset of the Points of (G_ (k,X)) st T is STAR holds

for S being Subset of X st S = meet T holds

( card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } )

let T be Subset of the Points of (G_ (k,X)); :: thesis: ( T is STAR implies for S being Subset of X st S = meet T holds

( card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } ) )

assume T is STAR ; :: thesis: for S being Subset of X st S = meet T holds

( card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } )

then consider S1 being Subset of X such that

A2: ( card S1 = k - 1 & T = { A where A is Subset of X : ( card A = k & S1 c= A ) } ) ;

let S be Subset of X; :: thesis: ( S = meet T implies ( card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } ) )

assume A3: S = meet T ; :: thesis: ( card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } )

S1 = meet T by A1, A2, Th26;

hence ( card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } ) by A3, A2; :: thesis: verum

for T being Subset of the Points of (G_ (k,X)) st T is STAR holds

for S being Subset of X st S = meet T holds

( card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } )

let X be non empty set ; :: thesis: ( 0 < k & k + 1 c= card X implies for T being Subset of the Points of (G_ (k,X)) st T is STAR holds

for S being Subset of X st S = meet T holds

( card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } ) )

assume A1: ( 0 < k & k + 1 c= card X ) ; :: thesis: for T being Subset of the Points of (G_ (k,X)) st T is STAR holds

for S being Subset of X st S = meet T holds

( card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } )

let T be Subset of the Points of (G_ (k,X)); :: thesis: ( T is STAR implies for S being Subset of X st S = meet T holds

( card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } ) )

assume T is STAR ; :: thesis: for S being Subset of X st S = meet T holds

( card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } )

then consider S1 being Subset of X such that

A2: ( card S1 = k - 1 & T = { A where A is Subset of X : ( card A = k & S1 c= A ) } ) ;

let S be Subset of X; :: thesis: ( S = meet T implies ( card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } ) )

assume A3: S = meet T ; :: thesis: ( card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } )

S1 = meet T by A1, A2, Th26;

hence ( card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } ) by A3, A2; :: thesis: verum