defpred S1[ Nat] means for L being finite Lattice
for X being Subset of (LattPOSet L)
for p being FinSequence st rng p = X & len p = $1 & not X is empty holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) );
let L be finite Lattice; :: thesis: for X being Subset of L holds
( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) )
let X be Subset of L; :: thesis: ( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) )
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; :: thesis: S1[k + 1]
per cases ( k = 0 or k <> 0 ) ;
suppose A3: k = 0 ; :: thesis: S1[k + 1]
for L being finite Lattice
for X being Subset of (LattPOSet L)
for p being FinSequence st rng p = X & len p = 1 holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) )
proof
let L be finite Lattice; :: thesis: for X being Subset of (LattPOSet L)
for p being FinSequence st rng p = X & len p = 1 holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) )
let X be Subset of (LattPOSet L); :: thesis: for p being FinSequence st rng p = X & len p = 1 holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) )
let p be FinSequence; :: thesis: ( rng p = X & len p = 1 implies ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) )
assume that
A4: rng p = X and
A5: len p = 1 ; :: thesis: ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) )
consider a being set such that
A6: p . 1 = a ;
A7: Seg 1 = dom p by A5, FINSEQ_1:def 3;
then 1 in dom p by FINSEQ_1:2, TARSKI:def 1;
then A8: a in rng p by A6, FUNCT_1:def 3;
then reconsider a = a as Element of (LattPOSet L) by A4;
rng p = {a} by A7, A6, FINSEQ_1:2, FUNCT_1:4;
then for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a by A4, TARSKI:def 1;
hence ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) by A4, A8; :: thesis: verum
end;
hence S1[k + 1] by A3; :: thesis: verum
end;
suppose A9: k <> 0 ; :: thesis: S1[k + 1]
for L being finite Lattice
for X being Subset of (LattPOSet L)
for p being FinSequence st rng p = X & len p = k + 1 holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) )
proof
let L be finite Lattice; :: thesis: for X being Subset of (LattPOSet L)
for p being FinSequence st rng p = X & len p = k + 1 holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) )
let X be Subset of (LattPOSet L); :: thesis: for p being FinSequence st rng p = X & len p = k + 1 holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) )
let p be FinSequence; :: thesis: ( rng p = X & len p = k + 1 implies ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) )
assume that
A10: rng p = X and
A11: len p = k + 1 ; :: thesis: ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) )
set q = p | (Seg k);
set X9 = rng (p | (Seg k));
A12: rng (p | (Seg k)) c= rng p by RELAT_1:70;
for x being object st x in rng (p | (Seg k)) holds
x in the carrier of (LattPOSet L)
proof
let x be object ; :: thesis: ( x in rng (p | (Seg k)) implies x in the carrier of (LattPOSet L) )
assume x in rng (p | (Seg k)) ; :: thesis: x in the carrier of (LattPOSet L)
then x in rng p by A12;
hence x in the carrier of (LattPOSet L) by A10; :: thesis: verum
end;
then A13: rng (p | (Seg k)) is Subset of (LattPOSet L) by TARSKI:def 3;
A14: k <= len p by A11, NAT_1:11;
then ( len (p | (Seg k)) = k & p | (Seg k) <> {} ) by A9, CARD_1:27, FINSEQ_1:17;
then consider a being Element of (LattPOSet L) such that
A15: a in rng (p | (Seg k)) and
A16: for b being Element of (LattPOSet L) st b in rng (p | (Seg k)) & b <> a holds
not b <= a by A2, A13;
consider b being set such that
A17: p . (k + 1) = b ;
Seg (k + 1) = dom p by A11, FINSEQ_1:def 3;
then k + 1 in dom p by FINSEQ_1:4;
then A18: b in rng p by A17, FUNCT_1:def 3;
then reconsider b = b as Element of (LattPOSet L) by A10;
per cases ( ex c being Element of (LattPOSet L) st
( c in X & c <= b & c <> b ) or for c being Element of (LattPOSet L) holds
( not c in X or not c <= b or not c <> b ) ) ;
suppose ex c being Element of (LattPOSet L) st
( c in X & c <= b & c <> b ) ; :: thesis: ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) )
then consider c being Element of (LattPOSet L) such that
A19: c in X and
A20: c <= b and
A21: c <> b ;
for u being Element of (LattPOSet L) st u in X & u <> a holds
not u <= a
proof
let u be Element of (LattPOSet L); :: thesis: ( u in X & u <> a implies not u <= a )
assume that
A22: u in X and
A23: u <> a ; :: thesis: not u <= a
per cases ( u in rng (p | (Seg k)) or not u in rng (p | (Seg k)) ) ;
suppose u in rng (p | (Seg k)) ; :: thesis: not u <= a
hence not u <= a by A16, A23; :: thesis: verum
end;
suppose A24: not u in rng (p | (Seg k)) ; :: thesis: not u <= a
consider n being object such that
A25: n in dom p and
A26: p . n = u by A10, A22, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A25;
A27: Seg (k + 1) = dom p by A11, FINSEQ_1:def 3;
then A28: n <= k + 1 by A25, FINSEQ_1:1;
A29: 1 <= n by A25, A27, FINSEQ_1:1;
A30: n = k + 1 A32: c in rng (p | (Seg k))
proof
consider n being object such that
A33: n in dom p and
A34: p . n = c by A10, A19, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A33;
A35: Seg (k + 1) = dom p by A11, FINSEQ_1:def 3;
then n <= k + 1 by A33, FINSEQ_1:1;
then n < k + 1 by A17, A21, A34, XXREAL_0:1;
then A36: n <= k by NAT_1:13;
1 <= n by A33, A35, FINSEQ_1:1;
then n in Seg k by A36, FINSEQ_1:1;
then A37: n in dom (p | (Seg k)) by A14, FINSEQ_1:17;
then (p | (Seg k)) . n = c by A34, FUNCT_1:47;
hence c in rng (p | (Seg k)) by A37, FUNCT_1:def 3; :: thesis: verum
end;
assume A38: u <= a ; :: thesis: contradiction
then c <> a by A17, A20, A21, A26, A30, ORDERS_2:2;
hence contradiction by A16, A17, A20, A26, A30, A38, A32, ORDERS_2:3; :: thesis: verum
end;
end;
end;
hence ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) by A10, A12, A15; :: thesis: verum
end;
suppose for c being Element of (LattPOSet L) holds
( not c in X or not c <= b or not c <> b ) ; :: thesis: ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) )
then for u being Element of (LattPOSet L) st u in X & u <> b holds
not u <= b ;
hence ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) by A10, A18; :: thesis: verum
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
end;
end;
A39: S1[ 0 ]
proof
let L be finite Lattice; :: thesis: for X being Subset of (LattPOSet L)
for p being FinSequence st rng p = X & len p = 0 & not X is empty holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) )
let X be Subset of (LattPOSet L); :: thesis: for p being FinSequence st rng p = X & len p = 0 & not X is empty holds
ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) )
let p be FinSequence; :: thesis: ( rng p = X & len p = 0 & not X is empty implies ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) )
assume that
A40: rng p = X and
A41: len p = 0 ; :: thesis: ( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) )
Seg 0 = dom p by A41, FINSEQ_1:def 3;
hence ( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) ) by A40, RELAT_1:42; :: thesis: verum
end;
A42: for k being Nat holds S1[k] from NAT_1:sch 2(A39, A1);
 reconsider X = X as finite Subset of L ;
LattPOSet L = RelStr(# the carrier of L,(LattRel L) #) by LATTICE3:def 2;
then reconsider X9 = X as finite Subset of (LattPOSet L) ;
consider p being FinSequence such that
A43: rng p = X9 by FINSEQ_1:52;
dom p = Seg (len p) by FINSEQ_1:def 3;
hence ( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) ) by A42, A43; :: thesis: verum