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 A1: ( 0 < k & 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
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 )
A2: k - 1 is Element of NAT by A1, NAT_1:20;
assume A4: ( card S = k - 1 & T = { A where A is Subset of X : ( card A = k & S c= A ) } ) ; :: thesis: S = meet T
then A5: S is finite by A2;
S = meet T

proof

A6: 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 A1, A2, NAT_1:40;
hence contradiction by XREAL_1:8; :: thesis: verum

end;

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

end;

A8: S c= meet T

proof

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 A9: a1 in T ; :: thesis: S c= a1
consider A1 being Subset of X such that
A10: ( a1 = A1 & card A1 = k & S c= A1 ) by A4, A9;
thus S c= a1 by A10; :: thesis: verum

end;

hence S c= meet T by A6, SETFAM_1:6; :: thesis: verum

end;

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

assume A12: not y in S ; :: thesis: contradiction
consider a1 being set such that
A13: a1 in T by A6, XBOOLE_0:def 1;
consider A1 being Subset of X such that
A14: ( a1 = A1 & card A1 = k & S c= A1 ) by A4, A13;
A15: ( y in a1 & card {y} = 1 ) by A11, A13, CARD_1:50, SETFAM_1:def 1;
then ( {y} c= a1 & a1 is finite ) by A14, ZFMISC_1:37;
then A16: card (a1 \ {y}) = k - 1 by A14, A15, CARD_2:63;
X \ a1 <> {}

proof

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

end;

then consider y2 being set such that
A17: y2 in X \ a1 by XBOOLE_0:def 1;
A18: ( not y2 in a1 \ {y} & a1 \ {y} is finite & a1 \ {y} c= X & {y2} c= X ) by A2, A14, A16, A17, XBOOLE_0:def 5, XBOOLE_1:1, ZFMISC_1:37;
then A19: ( card ((a1 \ {y}) \/ {y2}) = (k - 1) + 1 & (a1 \ {y}) \/ {y2} c= X ) by A16, CARD_2:54, XBOOLE_1:8;
A20: y2 <> y by A15, A17, XBOOLE_0:def 5;
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
A21: z in S /\ {y} by XBOOLE_0:def 1;
z in {y} by A21, XBOOLE_0:def 4;
then ( z in S & z = y ) by A21, TARSKI:def 1, XBOOLE_0:def 4;
hence contradiction by A12; :: thesis: verum

end;

then S c= a1 \ {y} by A14, XBOOLE_1:86;
then ( S c= (a1 \ {y}) \/ {y2} & S = a1 \ {y} ) by A4, A16, A18, CARD_FIN:1, XBOOLE_1:10;
then A22: ( (a1 \ {y}) \/ {y2} in T & not y in a1 \ {y} & not y in {y2} ) by A4, A12, A19, A20, TARSKI:def 1;
then not y in (a1 \ {y}) \/ {y2} by XBOOLE_0:def 3;
hence contradiction by A11, A22, SETFAM_1:def 1; :: thesis: verum

end;

hence y in S ; :: thesis: verum

end;

hence S = meet T by A8, XBOOLE_0:def 10; :: thesis: verum

end;

hence S = meet T ; :: thesis: verum