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

end;

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

end;

suppose A10: 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 A11: ( rng p = X & 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 X' = rng (p | (Seg k));
A12: k <= len p by A11, NAT_1:11;
then A13: len (p | (Seg k)) = k by FINSEQ_1:21;
A14: rng (p | (Seg k)) c= rng p by RELAT_1:99;
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 x in rng (p | (Seg k)) ; :: thesis: x in the carrier of (LattPOSet L)
then x in rng p by A14;
hence x in the carrier of (LattPOSet L) by A11; :: thesis: verum

end;

then A15: rng (p | (Seg k)) is Subset of (LattPOSet L) by TARSKI:def 3;
p | (Seg k) <> {} by A10, A13, CARD_1:47;
then rng (p | (Seg k)) <> {} ;
then consider a being Element of (LattPOSet L) such that
A16: ( a in rng (p | (Seg k)) & ( for b being Element of (LattPOSet L) st b in rng (p | (Seg k)) & b <> a holds
not a <= b ) ) by A4, A13, A15;
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:6;
then A18: b in rng p by A17, FUNCT_1:def 5;
then reconsider b = b as Element of (LattPOSet L) by A11;

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 & b <= c & 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 A20: ( u in X & u <> a ) ; :: thesis: not a <= u

now

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, A20; :: thesis: verum

end;

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

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

proof

assume n <> k + 1 ; :: thesis: contradiction
then n < k + 1 by A24, XXREAL_0:1;
then n <= k by NAT_1:13;
then n in Seg k by A24, FINSEQ_1:3;
then A26: n in dom (p | (Seg k)) by A12, FINSEQ_1:21;
then (p | (Seg k)) . n = u by A22, FUNCT_1:70;
hence contradiction by A21, A26, FUNCT_1:def 5; :: thesis: verum

end;

assume A27: a <= u ; :: thesis: not a <= u
A28: c in rng (p | (Seg k))

proof

consider n being set such that
A29: ( n in dom p & p . n = c ) by A11, A19, FUNCT_1:def 5;
A30: Seg (k + 1) = dom p by A11, FINSEQ_1:def 3;
reconsider n = n as Element of NAT by A29;
A31: ( 1 <= n & n <= k + 1 ) by A29, A30, FINSEQ_1:3;
then n < k + 1 by A17, A19, A29, XXREAL_0:1;
then n <= k by NAT_1:13;
then n in Seg k by A31, FINSEQ_1:3;
then A32: n in dom (p | (Seg k)) by A12, FINSEQ_1:21;
then (p | (Seg k)) . n = c by A29, FUNCT_1:70;
hence c in rng (p | (Seg k)) by A32, FUNCT_1:def 5; :: thesis: verum

end;

c <> a by A17, A19, A22, A25, A27, ORDERS_2:25;
hence not a <= u by A16, A17, A19, A22, A25, A28, ORDERS_2:26; :: 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 A11, A14, A16; :: 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 A11, A18; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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