defpred S₁[ 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 S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]

per cases ( k = 0 or k <> 0 ) ;

suppose A3: k = 0 ; :: thesis: S₁[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 S₁[k + 1] by A3; :: thesis: verum

end;

suppose A8: k <> 0 ; :: thesis: S₁[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

proof

assume not n >= k + 1 ; :: thesis: contradiction
then A27: n <= k by INT_1:7;
1 <= n by A25, FINSEQ_1:1;
then A28: n in Seg k by A27, FINSEQ_1:1;
dom (p | (Seg k)) = (dom p) /\ (Seg k) by RELAT_1:61
.= (Seg (k + 1)) /\ (Seg k) by A10, FINSEQ_1:def 3
.= Seg k by FINSEQ_1:7, NAT_1:11 ;
then A29: (p | (Seg k)) . n = c by A24, A28, FUNCT_1:47;
n in dom (p | (Seg k)) by A10, A14, A28, FINSEQ_1:17;
hence contradiction by A22, A29, FUNCT_1:def 3; :: thesis: verum

end;

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 S₁[k + 1] ; :: thesis: verum

end;

end;

end;

A30: S₁[ 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 S₁[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