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

proof

X \ S <> {}

proof

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

end;

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

end;

A9: meet T c= S

proof

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

proof

consider a1 being object such that
A11: a1 in T by A6, XBOOLE_0:def 1;
reconsider a1 = a1 as set by TARSKI:1;
A12: ex A1 being Subset of X st
( a1 = A1 & card A1 = k & S c= A1 ) by A4, A11;
then A13: a1 is finite ;
X \ a1 <> {}

proof

assume X \ a1 = {} ; :: thesis: contradiction
then X c= a1 by XBOOLE_1:37;
then card X = k by A12, XBOOLE_0:def 10;
then Segm (1 + k) c= Segm (0 + k) by A2;
then 1 + k <= 0 + k by NAT_1:39;
hence contradiction by XREAL_1:6; :: thesis: verum

end;

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

proof

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

end;

then S c= a1 \ {y} by A12, XBOOLE_1:86;
then A18: S c= (a1 \ {y}) \/ {y2} by XBOOLE_1:10;
A19: y in a1 by A10, A11, SETFAM_1:def 1;
then y2 <> y by A14, XBOOLE_0:def 5;
then A20: not y in {y2} by TARSKI:def 1;
( card {y} = 1 & {y} c= a1 ) by A19, CARD_1:30, ZFMISC_1:31;
then A21: card (a1 \ {y}) = k - 1 by A12, A13, CARD_2:44;
then not y in a1 \ {y} by A3, A15, A12, A13, A16, CARD_2:102, XBOOLE_1:86;
then A22: not y in (a1 \ {y}) \/ {y2} by A20, XBOOLE_0:def 3;
A23: {y2} c= X by A14, ZFMISC_1:31;
a1 \ {y} c= X by A12, XBOOLE_1:1;
then A24: (a1 \ {y}) \/ {y2} c= X by A23, XBOOLE_1:8;
not y2 in a1 \ {y} by A14, XBOOLE_0:def 5;
then card ((a1 \ {y}) \/ {y2}) = (k - 1) + 1 by A13, A21, CARD_2:41;
then (a1 \ {y}) \/ {y2} in T by A4, A24, A18;
hence contradiction by A10, A22, 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 A4;
hence S c= a1 ; :: thesis: verum

end;

then S c= meet T by A6, SETFAM_1:5;
hence S = meet T by A9, XBOOLE_0:def 10; :: thesis: verum