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 A2: ( T1 is STAR & T2 is STAR & meet T1 = meet T2 ) ; :: thesis: T1 = T2
consider S1 being Subset of X such that
A3: ( card S1 = k - 1 & T1 = { A where A is Subset of X : ( card A = k & S1 c= A ) } ) by A2, Def4;
consider S2 being Subset of X such that
A4: ( card S2 = k - 1 & T2 = { A where A is Subset of X : ( card A = k & S2 c= A ) } ) by A2, Def4;
( S1 = meet T1 & S2 = meet T2 ) by A1, A3, A4, Th26;
hence T1 = T2 by A2, A3, A4; :: thesis: verum