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 )
defpred S₁[ Element of 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;
A1: 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 A2: ( rng p = X & 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 )
then dom p = {} by FINSEQ_1:4, 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 A2, RELAT_1:65; :: thesis: verum

end;

A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]

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

suppose A5: 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 A6: ( rng p = X & 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
then A7: Seg 1 = dom p by FINSEQ_1:def 3;
consider a being set such that
A8: p . 1 = a ;
1 in dom p by A7, FINSEQ_1:4, TARSKI:def 1;
then a in rng p by A8, FUNCT_1:def 5;
then reconsider a = a as Element of (LattPOSet L) by A6;
rng p = {a} by A7, A8, FINSEQ_1:4, FUNCT_1:14;
then for b being Element of (LattPOSet L) st b in X holds
b <= a by A6, 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 A5; :: thesis: verum

end;

suppose A9: 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 A10: ( rng p = X & 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
set q = p | (Seg k);
set X' = rng (p | (Seg k));
A11: k <= k + 1 by NAT_1:11;
then A12: len (p | (Seg k)) = k by A10, FINSEQ_1:21;
for x being set st x in rng (p | (Seg k)) holds
x in the carrier of (LattPOSet L)

proof

let x be set ; :: thesis: ( x in rng (p | (Seg k)) implies x in the carrier of (LattPOSet L) )
assume A13: x in rng (p | (Seg k)) ; :: thesis: x in the carrier of (LattPOSet L)
rng (p | (Seg k)) c= rng p by RELAT_1:99;
then x in rng p by A13;
hence x in the carrier of (LattPOSet L) by A10; :: thesis: verum

end;

then A14: rng (p | (Seg k)) is Subset of (LattPOSet L) by TARSKI:def 3;
p | (Seg k) <> {} by A9, A12, CARD_1:47;
then rng (p | (Seg k)) <> {} ;
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 A4, A12, A14;
consider b being set such that
A16: p . (k + 1) = b ;
Seg (k + 1) = dom p by A10, FINSEQ_1:def 3;
then k + 1 in dom p by FINSEQ_1:6;
then b in rng p by A16, FUNCT_1:def 5;
then reconsider b = b as Element of (LattPOSet L) by A10;
set a2 = (% a) "\/" (% b);
A17: (% a) "\/" ((% a) "\/" (% b)) = ((% a) "\/" (% a)) "\/" (% b) by LATTICES:def 5
.= (% a) "\/" (% b) by LATTICES:17 ;
(% b) "\/" ((% a) "\/" (% b)) = ((% b) "\/" (% b)) "\/" (% a) by LATTICES:def 5
.= (% b) "\/" (% a) by LATTICES:17 ;
then A18: ( % a [= (% a) "\/" (% b) & % b [= (% a) "\/" (% b) ) by A17, LATTICES:def 3;
A19: (% a) % = % a by LATTICE3:def 3
.= a by LATTICE3:def 4 ;
A20: (% b) % = % b by LATTICE3:def 3
.= b 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 A21: 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 ( a <= ((% a) "\/" (% b)) % & c <= a ) by A15, A18, A19, LATTICE3:7;
hence c <= ((% a) "\/" (% b)) % by ORDERS_2:26; :: thesis: verum

end;

suppose A22: not c in rng (p | (Seg k)) ; :: thesis: c <= ((% a) "\/" (% b)) %

consider n being set such that
A23: ( n in dom p & c = p . n ) by A10, A21, FUNCT_1:def 5;
reconsider n = n as Element of NAT by A23;
A24: n in Seg (k + 1) by A10, A23, FINSEQ_1:def 3;
then A25: ( 1 <= n & n <= k + 1 ) by FINSEQ_1:3;
n >= k + 1

proof

assume not n >= k + 1 ; :: thesis: contradiction
then ( 1 <= n & n <= k ) by A24, FINSEQ_1:3, INT_1:20;
then A26: n in Seg k by FINSEQ_1:3;
then A27: n in dom (p | (Seg k)) by A10, A11, FINSEQ_1:21;
dom (p | (Seg k)) = (dom p) /\ (Seg k) by RELAT_1:90
.= (Seg (k + 1)) /\ (Seg k) by A10, FINSEQ_1:def 3
.= Seg k by FINSEQ_1:9, NAT_1:11 ;
then (p | (Seg k)) . n = c by A23, A26, FUNCT_1:70;
hence contradiction by A22, A27, FUNCT_1:def 5; :: thesis: verum

end;

then c = b by A16, A23, A25, XXREAL_0:1;
hence c <= ((% a) "\/" (% b)) % by A18, A20, 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;

A28: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A3);
reconsider X = X as finite Subset of L ;
LattPOSet L = RelStr(# the carrier of L,(LattRel L) #) by LATTICE3:def 2;
then reconsider X' = X as finite Subset of (LattPOSet L) ;
consider p being FinSequence such that
A29: rng p = X' by FINSEQ_1:73;
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 A28, A29; :: thesis: verum