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
for b being Element of (LattPOSet L) st b in X holds
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
for b being Element of (LattPOSet L) st b in X holds
b <= a )
let X be Subset of L; :: thesis: ( X is empty or ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
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
for b being Element of (LattPOSet L) st b in X holds
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
for b being Element of (LattPOSet L) st b in X holds
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
for b being Element of (LattPOSet L) st b in X holds
b <= a
let p be FinSequence; :: thesis: ( rng p = X & len p = 1 implies ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a )
assume that
A4: rng p = X and
A5: len p = 1 ; :: thesis: ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
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 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 holds
b <= a by A4, TARSKI:def 1;
hence ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a ; :: thesis: verum
end;
hence S1[k + 1] by A3; :: thesis: verum
end;
suppose A8: 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
for b being Element of (LattPOSet L) st b in X holds
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
for b being Element of (LattPOSet L) st b in X holds
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
for b being Element of (LattPOSet L) st b in X holds
b <= a
let p be FinSequence; :: thesis: ( rng p = X & len p = k + 1 implies ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a )
assume that
A9: rng p = X and
A10: len p = k + 1 ; :: thesis: ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a
consider b being set such that
A11: p . (k + 1) = b ;
set q = p | (Seg k);
set X9 = rng (p | (Seg k));
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) )
A12: rng (p | (Seg k)) c= rng p by RELAT_1:70;
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 A9; :: thesis: verum
end;
then A13: rng (p | (Seg k)) is Subset of (LattPOSet L) by TARSKI:def 3;
A14: k <= k + 1 by NAT_1:11;
then ( len (p | (Seg k)) = k & p | (Seg k) <> {} ) by A8, A10, CARD_1:27, FINSEQ_1:17;
then consider a being Element of (LattPOSet L) such that
A15: for b being Element of (LattPOSet L) st b in rng (p | (Seg k)) holds
b <= a by A2, A13;
Seg (k + 1) = dom p by A10, FINSEQ_1:def 3;
then k + 1 in dom p by FINSEQ_1:4;
then b in rng p by A11, FUNCT_1:def 3;
then reconsider b = b as Element of (LattPOSet L) by A9;
A16: (% b) % = % b by LATTICE3:def 3
.= b by LATTICE3:def 4 ;
set a2 = (% a) "\/" (% b);
(% a) "\/" ((% a) "\/" (% b)) = ((% a) "\/" (% a)) "\/" (% b) by LATTICES:def 5
.= (% a) "\/" (% b) ;
then A17: % a [= (% a) "\/" (% b) by LATTICES:def 3;
(% b) "\/" ((% a) "\/" (% b)) = ((% b) "\/" (% b)) "\/" (% a) by LATTICES:def 5
.= (% b) "\/" (% a) ;
then A18: % b [= (% a) "\/" (% b) by LATTICES:def 3;
A19: (% a) % = % a by LATTICE3:def 3
.= a by LATTICE3:def 4 ;
for c being Element of (LattPOSet L) st c in X holds
c <= ((% a) "\/" (% b)) %
proof
let c be Element of (LattPOSet L); :: thesis: ( c in X implies c <= ((% a) "\/" (% b)) % )
assume A20: c in X ; :: thesis: c <= ((% a) "\/" (% b)) %
per cases ( c in rng (p | (Seg k)) or not c in rng (p | (Seg k)) ) ;
suppose c in rng (p | (Seg k)) ; :: thesis: c <= ((% a) "\/" (% b)) %
then A21: c <= a by A15;
a <= ((% a) "\/" (% b)) % by A17, A19, LATTICE3:7;
hence c <= ((% a) "\/" (% b)) % by A21, ORDERS_2:3; :: thesis: verum
end;
suppose A22: not c in rng (p | (Seg k)) ; :: thesis: c <= ((% a) "\/" (% b)) %
consider n being object such that
A23: n in dom p and
A24: c = p . n by A9, A20, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A23;
A25: n in Seg (k + 1) by A10, A23, FINSEQ_1:def 3;
A26: n >= k + 1 n <= k + 1 by A25, FINSEQ_1:1;
then c = b by A11, A24, A26, XXREAL_0:1;
hence c <= ((% a) "\/" (% b)) % by A18, A16, LATTICE3:7; :: thesis: verum
end;
end;
end;
hence ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a ; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
end;
end;
A30: 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
for b being Element of (LattPOSet L) st b in X holds
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
for b being Element of (LattPOSet L) st b in X holds
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
for b being Element of (LattPOSet L) st b in X holds
b <= a )
assume that
A31: rng p = X and
A32: len p = 0 ; :: thesis: ( X is empty or ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a )
Seg (len p) = {} by A32;
then dom p = {} by FINSEQ_1:def 3;
hence ( X is empty or ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a ) by A31, RELAT_1:42; :: thesis: verum
end;
A33: for k being Nat holds S1[k] from NAT_1:sch 2(A30, 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
A34: 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
for b being Element of (LattPOSet L) st b in X holds
b <= a ) by A33, A34; :: thesis: verum