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

for T1, T2 being Subset of the Points of (G_ (k,X)) st T1 is STAR & T2 is STAR & meet T1 = meet T2 holds

T1 = T2

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

T1 = T2 )

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

T1 = T2

let T1, T2 be Subset of the Points of (G_ (k,X)); :: thesis: ( T1 is STAR & T2 is STAR & meet T1 = meet T2 implies T1 = T2 )

assume that

A2: T1 is STAR and

A3: T2 is STAR and

A4: meet T1 = meet T2 ; :: thesis: T1 = T2

consider S2 being Subset of X such that

A5: ( card S2 = k - 1 & T2 = { A where A is Subset of X : ( card A = k & S2 c= A ) } ) by A3;

A6: S2 = meet T2 by A1, A5, Th26;

consider S1 being Subset of X such that

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

S1 = meet T1 by A1, A7, Th26;

hence T1 = T2 by A4, A7, A5, A6; :: thesis: verum

for T1, T2 being Subset of the Points of (G_ (k,X)) st T1 is STAR & T2 is STAR & meet T1 = meet T2 holds

T1 = T2

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

T1 = T2 )

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

T1 = T2

let T1, T2 be Subset of the Points of (G_ (k,X)); :: thesis: ( T1 is STAR & T2 is STAR & meet T1 = meet T2 implies T1 = T2 )

assume that

A2: T1 is STAR and

A3: T2 is STAR and

A4: meet T1 = meet T2 ; :: thesis: T1 = T2

consider S2 being Subset of X such that

A5: ( card S2 = k - 1 & T2 = { A where A is Subset of X : ( card A = k & S2 c= A ) } ) by A3;

A6: S2 = meet T2 by A1, A5, Th26;

consider S1 being Subset of X such that

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

S1 = meet T1 by A1, A7, Th26;

hence T1 = T2 by A4, A7, A5, A6; :: thesis: verum