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 object 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 object 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 object 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 ) by ORDERS_2:def 5, A6;
( the InternalRel of ((LattPOSet L) ~) -Seg a) /\ Y = {}
proof
set z = the Element of ( the InternalRel of ((LattPOSet L) ~) -Seg a) /\ Y;
assume A9: ( the InternalRel of ((LattPOSet L) ~) -Seg a) /\ Y <> {} ; :: thesis: contradiction
then the Element of ( the InternalRel of ((LattPOSet L) ~) -Seg a) /\ Y in the InternalRel of ((LattPOSet L) ~) -Seg a by XBOOLE_0:def 4;
then A10: ( the Element of ( the InternalRel of ((LattPOSet L) ~) -Seg a) /\ Y <> a & [ the Element of ( the InternalRel of ((LattPOSet L) ~) -Seg a) /\ Y,a] in the InternalRel of ((LattPOSet L) ~) ) by WELLORD1:1;
the Element of ( the InternalRel of ((LattPOSet L) ~) -Seg a) /\ Y in Y by A9, XBOOLE_0:def 4;
hence contradiction by A2, A8, A10; :: thesis: verum
end;
then the InternalRel of ((LattPOSet L) ~) -Seg a misses Y by XBOOLE_0:def 7;
hence ex a being object 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) ~) ;
hence (LattPOSet L) ~ is well_founded ; :: thesis: verum