let L be finite Lattice; :: thesis: (LattPOSet L) ~ is well_founded
set R = LattPOSet L;
A1: (LattPOSet L) ~ = RelStr(# the carrier of (LattPOSet L),(the InternalRel of (LattPOSet L) ~ ) #) by LATTICE3:def 5;
for Y being set st Y c= the carrier of ((LattPOSet L) ~ ) & Y <> {} holds
ex a being set st
( a in Y & the InternalRel of ((LattPOSet L) ~ ) -Seg a misses Y )

proof

let Y be set ; :: thesis: ( Y c= the carrier of ((LattPOSet L) ~ ) & Y <> {} implies ex a being set st
( a in Y & the InternalRel of ((LattPOSet L) ~ ) -Seg a misses Y ) )
assume A2: ( Y c= the carrier of ((LattPOSet L) ~ ) & Y <> {} ) ; :: thesis: ex a being set st
( a in Y & the InternalRel of ((LattPOSet L) ~ ) -Seg a misses Y )
LattPOSet L = RelStr(# the carrier of L,(LattRel L) #) by LATTICE3:def 2;
then reconsider Y = Y as Subset of L by A1, A2;
consider a being Element of (LattPOSet L) such that
A3: ( a in Y & ( for b being Element of (LattPOSet L) st b in Y & b <> a holds
not a <= b ) ) by A2, Lm2;
reconsider a = a as Element of (LattPOSet L) ;
reconsider a' = a as Element of ((LattPOSet L) ~ ) by A1;
A4: for b being Element of ((LattPOSet L) ~ ) st b in Y & b <> a holds
not b <= a'

proof

let b be Element of ((LattPOSet L) ~ ); :: thesis: ( b in Y & b <> a implies not b <= a' )
assume A5: ( b in Y & b <> a ) ; :: thesis: not b <= a'
reconsider b' = b as Element of (LattPOSet L) by A1;
A6: not a <= b' by A3, A5;
( a ~ = a' & b' ~ = b ) by LATTICE3:def 6;
hence not b <= a' by A6, LATTICE3:9; :: thesis: verum

end;

A7: for x being Element of ((LattPOSet L) ~ ) holds
( not x <> a or not [x,a] in the InternalRel of ((LattPOSet L) ~ ) or not x in Y )

proof

given x being Element of ((LattPOSet L) ~ ) such that A8: ( x <> a & [x,a] in the InternalRel of ((LattPOSet L) ~ ) & x in Y ) ; :: thesis: contradiction
x <= a' by A8, ORDERS_2:def 9;
hence contradiction by A4, A8; :: thesis: verum

end;

(the InternalRel of ((LattPOSet L) ~ ) -Seg a) /\ Y = {}

proof

assume A9: (the InternalRel of ((LattPOSet L) ~ ) -Seg a) /\ Y <> {} ; :: thesis: contradiction
consider z being Element of (the InternalRel of ((LattPOSet L) ~ ) -Seg a) /\ Y;
A10: ( z in the InternalRel of ((LattPOSet L) ~ ) -Seg a & z in Y ) by A9, XBOOLE_0:def 4;
then ( z <> a & [z,a] in the InternalRel of ((LattPOSet L) ~ ) ) by WELLORD1:def 1;
hence contradiction by A2, A7, A10; :: thesis: verum

end;

then the InternalRel of ((LattPOSet L) ~ ) -Seg a misses Y by XBOOLE_0:def 7;
hence ex a being set st
( a in Y & the InternalRel of ((LattPOSet L) ~ ) -Seg a misses Y ) by A3; :: thesis: verum

end;

then the InternalRel of ((LattPOSet L) ~ ) is_well_founded_in the carrier of ((LattPOSet L) ~ ) by WELLORD1:def 3;
hence (LattPOSet L) ~ is well_founded by WELLFND1:def 2; :: thesis: verum