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 that
A2: Y c= the carrier of ((LattPOSet L) ~) and
A3: 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
A4: a in Y and
A5: for b being Element of (LattPOSet L) st b in Y & b <> a holds
not a <= b by A3, Lm2;
reconsider a = a as Element of (LattPOSet L) ;
reconsider a9 = a as Element of ((LattPOSet L) ~) by A1;
A6: for b being Element of ((LattPOSet L) ~) st b in Y & b <> a holds
not b <= a9

proof

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

end;

A8: 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 A9: x <> a and
A10: [x,a] in the InternalRel of ((LattPOSet L) ~) and
A11: x in Y ; :: thesis: contradiction
x <= a9 by A10, ORDERS_2:def 9;
hence contradiction by A6, A9, A11; :: thesis: verum

end;

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

proof

consider z being Element of ( the InternalRel of ((LattPOSet L) ~) -Seg a) /\ Y;
assume A12: ( the InternalRel of ((LattPOSet L) ~) -Seg a) /\ Y <> {} ; :: thesis: contradiction
then z in the InternalRel of ((LattPOSet L) ~) -Seg a by XBOOLE_0:def 4;
then A13: ( z <> a & [z,a] in the InternalRel of ((LattPOSet L) ~) ) by WELLORD1:def 1;
z in Y by A12, XBOOLE_0:def 4;
hence contradiction by A2, A8, A13; :: 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 A4; :: 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