let k be Element of NAT ; 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 ; ( 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 )
; 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)); ( 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
; 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; verum