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
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) );
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 a <= b ) ) )
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 a <= b ) ) )
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
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) )

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

end;

hence S₁[k + 1] by A3; :: 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
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) )

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 a <= b ) )
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 a <= b ) )
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 a <= b ) ) )
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 a <= b ) )
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 a <= b 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 & b <= c & c <> b ) or for c being Element of (LattPOSet L) holds
( not c in X or not b <= c or not c <> b ) ) ;

suppose ex c being Element of (LattPOSet L) st
( c in X & b <= c & 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 a <= b ) )

then consider c being Element of (LattPOSet L) such that
A19: c in X and
A20: b <= c and
A21: c <> b ;
for u being Element of (LattPOSet L) st u in X & u <> a holds
not a <= u

proof

let u be Element of (LattPOSet L); :: thesis: ( u in X & u <> a implies not a <= u )
assume that
A22: u in X and
A23: u <> a ; :: thesis: not a <= u

now :: thesis: ( ( u in rng (p | (Seg k)) & not a <= u ) or ( not u in rng (p | (Seg k)) & ( a <= u implies not a <= u ) ) )

per cases ( u in rng (p | (Seg k)) or not u in rng (p | (Seg k)) ) ;

case u in rng (p | (Seg k)) ; :: thesis: not a <= u

hence not a <= u by A16, A23; :: thesis: verum

end;

case A24: not u in rng (p | (Seg k)) ; :: thesis: ( a <= u implies not a <= u )

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

proof

assume n <> k + 1 ; :: thesis: contradiction
then n < k + 1 by A28, XXREAL_0:1;
then n <= k by NAT_1:13;
then n in Seg k by A29, FINSEQ_1:1;
then A31: n in dom (p | (Seg k)) by A14, FINSEQ_1:17;
then (p | (Seg k)) . n = u by A26, FUNCT_1:47;
hence contradiction by A24, A31, FUNCT_1:def 3; :: thesis: verum

end;

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 a <= u ; :: thesis: not a <= u
then c <> a by A17, A20, A21, A26, A30, ORDERS_2:2;
hence not a <= u by A16, A17, A20, A26, A30, A32, ORDERS_2:3; :: thesis: verum

end;

end;

end;

hence not a <= u ; :: thesis: verum

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 a <= b ) ) by A10, A12, A15; :: thesis: verum

end;

suppose for c being Element of (LattPOSet L) holds
( not c in X or not b <= c 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 a <= b ) )

then for u being Element of (LattPOSet L) st u in X & u <> b holds
not b <= u ;
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 a <= b ) ) by A10, A18; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

end;

end;

A38: 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
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) )
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 a <= b ) )
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 a <= b ) ) )
assume that
A39: rng p = X and
A40: 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 a <= b ) ) )
Seg 0 = dom p by A40, 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 a <= b ) ) ) by A39, RELAT_1:42; :: thesis: verum

end;

A41: for k being Nat holds S₁[k] from NAT_1:sch 2(A38, 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
A42: 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 a <= b ) ) ) by A41, A42; :: thesis: verum