let L be upper-bounded LATTICE; :: thesis: for l being Element of L st l <> Top L holds
( l is prime iff (downarrow l) ` is Filter of L )
let l be Element of L; :: thesis: ( l <> Top L implies ( l is prime iff (downarrow l) ` is Filter of L ) )
set X1 = the carrier of L \ (downarrow l);
reconsider X = the carrier of L \ (downarrow l) as Subset of L ;
assume A1: l <> Top L ; :: thesis: ( l is prime iff (downarrow l) ` is Filter of L )
thus ( l is prime implies (downarrow l) ` is Filter of L ) :: thesis: ( (downarrow l) ` is Filter of L implies l is prime )
proof
assume A2: l is prime ; :: thesis: (downarrow l) ` is Filter of L
A3: now :: thesis: for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X & z <= x & z <= y )
let x, y be Element of L; :: thesis: ( x in X & y in X implies ex z being Element of L st
( z in X & z <= x & z <= y ) )
assume that
A4: x in X and
A5: y in X ; :: thesis: ex z being Element of L st
( z in X & z <= x & z <= y )
not y in downarrow l by A5, XBOOLE_0:def 5;
then A6: not y <= l by WAYBEL_0:17;
not x in downarrow l by A4, XBOOLE_0:def 5;
then A7: not x <= l by WAYBEL_0:17;
not x "/\" y in downarrow l by A2, A7, A6, WAYBEL_0:17;
then A8: x "/\" y in X by XBOOLE_0:def 5;
( x "/\" y <= x & x "/\" y <= y ) by YELLOW_0:23;
hence ex z being Element of L st
( z in X & z <= x & z <= y ) by A8; :: thesis: verum
end;
A9: now :: thesis: for x, y being Element of L st x in X & x <= y holds
y in X
let x, y be Element of L; :: thesis: ( x in X & x <= y implies y in X )
assume that
A10: x in X and
A11: x <= y ; :: thesis: y in X
not x in downarrow l by A10, XBOOLE_0:def 5;
then not x <= l by WAYBEL_0:17;
then not y <= l by A11, ORDERS_2:3;
then not y in downarrow l by WAYBEL_0:17;
hence y in X by XBOOLE_0:def 5; :: thesis: verum
end;
now :: thesis: not Top L in downarrow l
assume Top L in downarrow l ; :: thesis: contradiction
then Top L <= l by WAYBEL_0:17;
then Top L < l by A1, ORDERS_2:def 6;
hence contradiction by ORDERS_2:6, YELLOW_0:45; :: thesis: verum
end;
hence (downarrow l) ` is Filter of L by A3, A9, WAYBEL_0:def 2, WAYBEL_0:def 20, XBOOLE_0:def 5; :: thesis: verum
end;
thus ( (downarrow l) ` is Filter of L implies l is prime ) :: thesis: verum
proof
l <= l ;
then A12: l in downarrow l by WAYBEL_0:17;
assume A13: (downarrow l) ` is Filter of L ; :: thesis: l is prime
let x, y be Element of L; :: according to WAYBEL_6:def 6 :: thesis: ( not x "/\" y <= l or x <= l or y <= l )
assume A14: x "/\" y <= l ; :: thesis: ( x <= l or y <= l )
now :: thesis: ( not x <= l implies y <= l )
assume that
A15: not x <= l and
A16: not y <= l ; :: thesis: contradiction
not y in downarrow l by A16, WAYBEL_0:17;
then A17: y in X by XBOOLE_0:def 5;
not x in downarrow l by A15, WAYBEL_0:17;
then x in X by XBOOLE_0:def 5;
then consider z being Element of L such that
A18: z in X and
A19: ( z <= x & z <= y ) by A13, A17, WAYBEL_0:def 2;
z <= x "/\" y by A19, YELLOW_0:23;
then z <= l by A14, ORDERS_2:3;
then l in X by A13, A18, WAYBEL_0:def 20;
hence contradiction by A12, XBOOLE_0:def 5; :: thesis: verum
end;
hence ( x <= l or y <= l ) ; :: thesis: verum
end;