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)
for S being Subset of X st card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } holds
S = meet T
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)
for S being Subset of X st card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } holds
S = meet T )
assume that
A1: 0 < k and
A2: k + 1 c= card X ; :: thesis: for T being Subset of the Points of (G_ k,X)
for S being Subset of X st card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } holds
S = meet T
A3: k - 1 is Element of NAT by A1, NAT_1:20;
let T be Subset of the Points of (G_ k,X); :: thesis: for S being Subset of X st card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } holds
S = meet T
let S be Subset of X; :: thesis: ( card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } implies S = meet T )
assume that
A4: card S = k - 1 and
A5: T = { A where A is Subset of X : ( card A = k & S c= A ) } ; :: thesis: S = meet T
A6: S is finite by A1, A4, NAT_1:20;
A7: T <> {}

proof

X \ S <> {}

proof

assume X \ S = {} ; :: thesis: contradiction
then X c= S by XBOOLE_1:37;
then card X = k - 1 by A4, XBOOLE_0:def 10;
then 1 + k <= (- 1) + k by A2, A3, NAT_1:40;
hence contradiction by XREAL_1:8; :: thesis: verum

end;

then consider x being set such that
A8: x in X \ S by XBOOLE_0:def 1;
{x} c= X by A8, ZFMISC_1:37;
then A9: ( S c= S \/ {x} & S \/ {x} c= X ) by XBOOLE_1:7, XBOOLE_1:8;
not x in S by A8, XBOOLE_0:def 5;
then card (S \/ {x}) = (k - 1) + 1 by A4, A6, CARD_2:54;
then S \/ {x} in T by A5, A9;
hence T <> {} ; :: thesis: verum

end;

A10: meet T c= S

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in meet T or y in S )
assume A11: y in meet T ; :: thesis: y in S
y in S

proof

consider a1 being set such that
A12: a1 in T by A7, XBOOLE_0:def 1;
A13: ex A1 being Subset of X st
( a1 = A1 & card A1 = k & S c= A1 ) by A5, A12;
then A14: a1 is finite ;
X \ a1 <> {}

proof

assume X \ a1 = {} ; :: thesis: contradiction
then X c= a1 by XBOOLE_1:37;
then card X = k by A13, XBOOLE_0:def 10;
then 1 + k <= 0 + k by A2, NAT_1:40;
hence contradiction by XREAL_1:8; :: thesis: verum

end;

then consider y2 being set such that
A15: y2 in X \ a1 by XBOOLE_0:def 1;
assume A16: not y in S ; :: thesis: contradiction
A17: S misses {y}

proof

assume not S misses {y} ; :: thesis: contradiction
then S /\ {y} <> {} by XBOOLE_0:def 7;
then consider z being set such that
A18: z in S /\ {y} by XBOOLE_0:def 1;
( z in {y} & z in S ) by A18, XBOOLE_0:def 4;
hence contradiction by A16, TARSKI:def 1; :: thesis: verum

end;

then S c= a1 \ {y} by A13, XBOOLE_1:86;
then A19: S c= (a1 \ {y}) \/ {y2} by XBOOLE_1:10;
A20: y in a1 by A11, A12, SETFAM_1:def 1;
then y2 <> y by A15, XBOOLE_0:def 5;
then A21: not y in {y2} by TARSKI:def 1;
( card {y} = 1 & {y} c= a1 ) by A20, CARD_1:50, ZFMISC_1:37;
then A22: card (a1 \ {y}) = k - 1 by A13, A14, CARD_2:63;
then not y in a1 \ {y} by A4, A16, A13, A14, A17, CARD_FIN:1, XBOOLE_1:86;
then A23: not y in (a1 \ {y}) \/ {y2} by A21, XBOOLE_0:def 3;
A24: {y2} c= X by A15, ZFMISC_1:37;
a1 \ {y} c= X by A13, XBOOLE_1:1;
then A25: (a1 \ {y}) \/ {y2} c= X by A24, XBOOLE_1:8;
not y2 in a1 \ {y} by A15, XBOOLE_0:def 5;
then card ((a1 \ {y}) \/ {y2}) = (k - 1) + 1 by A14, A22, CARD_2:54;
then (a1 \ {y}) \/ {y2} in T by A5, A25, A19;
hence contradiction by A11, A23, SETFAM_1:def 1; :: thesis: verum

end;

hence y in S ; :: thesis: verum

end;

for a1 being set st a1 in T holds
S c= a1

proof

let a1 be set ; :: thesis: ( a1 in T implies S c= a1 )
assume a1 in T ; :: thesis: S c= a1
then ex A1 being Subset of X st
( a1 = A1 & card A1 = k & S c= A1 ) by A5;
hence S c= a1 ; :: thesis: verum

end;

then S c= meet T by A7, SETFAM_1:6;
hence S = meet T by A10, XBOOLE_0:def 10; :: thesis: verum