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 <> {}

S c= a1

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

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

A9:
meet T c= S
X \ S <> {}

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;proof

then consider x being object such that
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 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

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

proof

for a1 being set st a1 in T holds
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

end;assume A10: y in meet T ; :: thesis: y in S

y in S

proof

hence
y in S
; :: thesis: verum
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 <> {}

A14: y2 in X \ a1 by XBOOLE_0:def 1;

assume A15: not y in S ; :: thesis: contradiction

A16: S misses {y}

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;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

then consider y2 being object such that
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 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

A14: y2 in X \ a1 by XBOOLE_0:def 1;

assume A15: not y in S ; :: thesis: contradiction

A16: S misses {y}

proof

then
S c= a1 \ {y}
by A12, XBOOLE_1:86;
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 /\ {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

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

S c= a1

proof

then
S c= meet T
by A6, SETFAM_1:5;
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;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

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