let L be complete LATTICE; :: thesis: for x being Element of L holds meet { ((DownMap I) . x) where I is Ideal of L : verum } = waybelow x
let x be Element of L; :: thesis: meet { ((DownMap I) . x) where I is Ideal of L : verum } = waybelow x
set A = { ((DownMap I) . x) where I is Ideal of L : verum } ;
set A1 = { ((DownMap I) . x) where I is Ideal of L : x <= sup I } ;
A1: { ((DownMap I) . x) where I is Ideal of L : x <= sup I } c= { ((downarrow x) /\ I) where I is Ideal of L : x <= sup I }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } or a in { ((downarrow x) /\ I) where I is Ideal of L : x <= sup I } )
assume a in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } ; :: thesis: a in { ((downarrow x) /\ I) where I is Ideal of L : x <= sup I }
then consider I1 being Ideal of L such that
A2: a = (DownMap I1) . x and
A3: x <= sup I1 ;
a = (downarrow x) /\ I1 by A2, A3, Def16;
hence a in { ((downarrow x) /\ I) where I is Ideal of L : x <= sup I } by A3; :: thesis: verum

end;

{ ((downarrow x) /\ I) where I is Ideal of L : x <= sup I } c= { ((DownMap I) . x) where I is Ideal of L : x <= sup I }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((downarrow x) /\ I) where I is Ideal of L : x <= sup I } or a in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } )
assume a in { ((downarrow x) /\ I) where I is Ideal of L : x <= sup I } ; :: thesis: a in { ((DownMap I) . x) where I is Ideal of L : x <= sup I }
then consider I1 being Ideal of L such that
A4: a = (downarrow x) /\ I1 and
A5: x <= sup I1 ;
a = (DownMap I1) . x by A4, A5, Def16;
hence a in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } by A5; :: thesis: verum

end;

then A6: { ((DownMap I) . x) where I is Ideal of L : x <= sup I } = { ((downarrow x) /\ I) where I is Ideal of L : x <= sup I } by A1;
set A2 = { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } ;
A7: { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } c= { (downarrow x) where I is Ideal of L : not x <= sup I }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } or a in { (downarrow x) where I is Ideal of L : not x <= sup I } )
assume a in { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } ; :: thesis: a in { (downarrow x) where I is Ideal of L : not x <= sup I }
then A8: ex I1 being Ideal of L st
( a = (DownMap I1) . x & not x <= sup I1 ) ;
then a = downarrow x by Def16;
hence a in { (downarrow x) where I is Ideal of L : not x <= sup I } by A8; :: thesis: verum

end;

{ (downarrow x) where I is Ideal of L : not x <= sup I } c= { ((DownMap I) . x) where I is Ideal of L : not x <= sup I }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (downarrow x) where I is Ideal of L : not x <= sup I } or a in { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } )
assume a in { (downarrow x) where I is Ideal of L : not x <= sup I } ; :: thesis: a in { ((DownMap I) . x) where I is Ideal of L : not x <= sup I }
then consider I1 being Ideal of L such that
A9: a = downarrow x and
A10: not x <= sup I1 ;
a = (DownMap I1) . x by A9, A10, Def16;
hence a in { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } by A10; :: thesis: verum

end;

then A11: { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } = { (downarrow x) where I is Ideal of L : not x <= sup I } by A7;
A12: { ((DownMap I) . x) where I is Ideal of L : verum } c= { ((DownMap I) . x) where I is Ideal of L : x <= sup I } \/ { ((DownMap I) . x) where I is Ideal of L : not x <= sup I }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((DownMap I) . x) where I is Ideal of L : verum } or a in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } \/ { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } )
assume a in { ((DownMap I) . x) where I is Ideal of L : verum } ; :: thesis: a in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } \/ { ((DownMap I) . x) where I is Ideal of L : not x <= sup I }
then consider I2 being Ideal of L such that
A13: a = (DownMap I2) . x ;
( x <= sup I2 or not x <= sup I2 ) ;
then ( a in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } or a in { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } ) by A13;
hence a in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } \/ { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } by XBOOLE_0:def 3; :: thesis: verum

end;

{ ((DownMap I) . x) where I is Ideal of L : x <= sup I } \/ { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } c= { ((DownMap I) . x) where I is Ideal of L : verum }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } \/ { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } or a in { ((DownMap I) . x) where I is Ideal of L : verum } )
assume a in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } \/ { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } ; :: thesis: a in { ((DownMap I) . x) where I is Ideal of L : verum }
then ( a in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } or a in { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } ) by XBOOLE_0:def 3;
then consider I2, I3 being Ideal of L such that
A14: ( ( a = (DownMap I2) . x & x <= sup I2 ) or ( a = (DownMap I3) . x & not x <= sup I3 ) ) ;

per cases ( ( a = (DownMap I2) . x & x <= sup I2 ) or ( a = (DownMap I3) . x & not x <= sup I3 ) ) by A14;

suppose ( a = (DownMap I2) . x & x <= sup I2 ) ; :: thesis: a in { ((DownMap I) . x) where I is Ideal of L : verum }

hence a in { ((DownMap I) . x) where I is Ideal of L : verum } ; :: thesis: verum

end;

suppose ( a = (DownMap I3) . x & not x <= sup I3 ) ; :: thesis: a in { ((DownMap I) . x) where I is Ideal of L : verum }

hence a in { ((DownMap I) . x) where I is Ideal of L : verum } ; :: thesis: verum

end;

end;

end;

then A15: { ((DownMap I) . x) where I is Ideal of L : verum } = { ((DownMap I) . x) where I is Ideal of L : x <= sup I } \/ { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } by A12;

per cases ( x = Bottom L or Bottom L <> x ) ;

suppose A16: x = Bottom L ; :: thesis: meet { ((DownMap I) . x) where I is Ideal of L : verum } = waybelow x

A17: { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } = {}

proof

assume { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } <> {} ; :: thesis: contradiction
then reconsider A29 = { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } as non empty set ;
set a = the Element of A29;
the Element of A29 in A29 ;
then ex I1 being Ideal of L st
( the Element of A29 = downarrow x & not x <= sup I1 ) by A11;
hence contradiction by A16, YELLOW_0:44; :: thesis: verum

end;

set Dx = downarrow x;
x <= sup (downarrow x) by A16, YELLOW_0:44;
then A18: (downarrow x) /\ (downarrow x) in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } by A6;
{ ((DownMap I) . x) where I is Ideal of L : x <= sup I } c= { K where K is Ideal of L : x <= sup K }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } or a in { K where K is Ideal of L : x <= sup K } )
assume a in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } ; :: thesis: a in { K where K is Ideal of L : x <= sup K }
then ex H being Ideal of L st
( a = (downarrow x) /\ H & x <= sup H ) by A6;
then reconsider a9 = a as Ideal of L by YELLOW_2:40;
x <= sup a9 by A16, YELLOW_0:44;
hence a in { K where K is Ideal of L : x <= sup K } ; :: thesis: verum

end;

then A19: meet { K where K is Ideal of L : x <= sup K } c= meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I } by A18, SETFAM_1:6;
A20: meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I } = {x}

proof

reconsider I9 = downarrow x as Ideal of L ;
x <= sup I9 by A16, YELLOW_0:44;
then (downarrow x) /\ I9 in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } by A6;
then {x} in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } by A16, Th23;
hence meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I } c= {x} by SETFAM_1:3; :: according to XBOOLE_0:def 10 :: thesis: {x} c= meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I }
for Z1 being set st Z1 in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } holds
{x} c= Z1

proof

let Z1 be set ; :: thesis: ( Z1 in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } implies {x} c= Z1 )
assume Z1 in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } ; :: thesis: {x} c= Z1
then consider Z19 being Ideal of L such that
A21: Z1 = (downarrow x) /\ Z19 and
x <= sup Z19 by A6;
A22: {x} c= Z19 by A16, Lm4;
{x} c= downarrow x by A16, Th23;
hence {x} c= Z1 by A21, A22, XBOOLE_1:19; :: thesis: verum

end;

hence {x} c= meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I } by A18, SETFAM_1:5; :: thesis: verum

end;

set E = the Ideal of L;
x <= sup the Ideal of L by A16, YELLOW_0:44;
then A23: the Ideal of L in { K where K is Ideal of L : x <= sup K } ;
for Z1 being set st Z1 in { K where K is Ideal of L : x <= sup K } holds
meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I } c= Z1

proof

let Z1 be set ; :: thesis: ( Z1 in { K where K is Ideal of L : x <= sup K } implies meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I } c= Z1 )
assume Z1 in { K where K is Ideal of L : x <= sup K } ; :: thesis: meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I } c= Z1
then ex K1 being Ideal of L st
( K1 = Z1 & x <= sup K1 ) ;
hence meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I } c= Z1 by A16, A20, Lm4; :: thesis: verum

end;

then meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I } c= meet { K where K is Ideal of L : x <= sup K } by A23, SETFAM_1:5;
then meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I } = meet { K where K is Ideal of L : x <= sup K } by A19;
hence meet { ((DownMap I) . x) where I is Ideal of L : verum } = waybelow x by A15, A17, Th34; :: thesis: verum

end;

suppose A24: Bottom L <> x ; :: thesis: meet { ((DownMap I) . x) where I is Ideal of L : verum } = waybelow x

set O = downarrow (Bottom L);
A25: sup (downarrow (Bottom L)) = Bottom L by WAYBEL_0:34;
then not x < sup (downarrow (Bottom L)) by ORDERS_2:6, YELLOW_0:44;
then not x <= sup (downarrow (Bottom L)) by A24, A25, ORDERS_2:def 6;
then A26: downarrow x in { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } by A11;
reconsider O1 = downarrow x as Ideal of L ;
A27: x <= sup O1 by WAYBEL_0:34;
downarrow x = (downarrow x) /\ O1 ;
then A28: downarrow x in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } by A6, A27;
A29: meet { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } c= downarrow x by A26, SETFAM_1:3;

now :: thesis: for Z1 being set st Z1 in { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } holds
downarrow x c= Z1

let Z1 be set ; :: thesis: ( Z1 in { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } implies downarrow x c= Z1 )
assume Z1 in { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } ; :: thesis: downarrow x c= Z1
then ex L1 being Ideal of L st
( Z1 = downarrow x & not x <= sup L1 ) by A11;
hence downarrow x c= Z1 ; :: thesis: verum

end;

then downarrow x c= meet { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } by A26, SETFAM_1:5;
then A30: meet { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } = downarrow x by A29;
A31: meet { ((DownMap I) . x) where I is Ideal of L : verum } = (meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I } ) /\ (meet { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } ) by A15, A26, A28, SETFAM_1:9;
A32: meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I } c= downarrow x by A28, SETFAM_1:3;
A33: meet { ((DownMap I) . x) where I is Ideal of L : verum } = meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I } by A28, A30, A31, SETFAM_1:3, XBOOLE_1:28;
A34: meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I } c= (downarrow x) /\ (meet { I where I is Ideal of L : x <= sup I } )

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I } or a in (downarrow x) /\ (meet { I where I is Ideal of L : x <= sup I } ) )
assume A35: a in meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I } ; :: thesis: a in (downarrow x) /\ (meet { I where I is Ideal of L : x <= sup I } )
thus a in (downarrow x) /\ (meet { I where I is Ideal of L : x <= sup I } ) :: thesis: verum

proof

reconsider L9 = [#] L as Subset of L ;
ex_sup_of L9,L by YELLOW_0:17;
then L9 is_<=_than sup L9 by YELLOW_0:def 9;
then x <= sup L9 ;
then A36: L9 in { I where I is Ideal of L : x <= sup I } ;

now :: thesis: for Y1 being set st Y1 in { I where I is Ideal of L : x <= sup I } holds
a in Y1

let Y1 be set ; :: thesis: ( Y1 in { I where I is Ideal of L : x <= sup I } implies a in Y1 )
assume Y1 in { I where I is Ideal of L : x <= sup I } ; :: thesis: a in Y1
then consider Y19 being Ideal of L such that
A37: Y1 = Y19 and
A38: x <= sup Y19 ;
A39: (downarrow x) /\ Y19 c= Y19 by XBOOLE_1:17;
(downarrow x) /\ Y19 in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } by A6, A38;
then a in (downarrow x) /\ Y19 by A35, SETFAM_1:def 1;
hence a in Y1 by A37, A39; :: thesis: verum

end;

then a in meet { I where I is Ideal of L : x <= sup I } by A36, SETFAM_1:def 1;
hence a in (downarrow x) /\ (meet { I where I is Ideal of L : x <= sup I } ) by A32, A35, XBOOLE_0:def 4; :: thesis: verum

end;

end;

(downarrow x) /\ (meet { I where I is Ideal of L : x <= sup I } ) c= meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (downarrow x) /\ (meet { I where I is Ideal of L : x <= sup I } ) or a in meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I } )
assume A40: a in (downarrow x) /\ (meet { I where I is Ideal of L : x <= sup I } ) ; :: thesis: a in meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I }
then A41: a in downarrow x by XBOOLE_0:def 4;
A42: a in meet { I where I is Ideal of L : x <= sup I } by A40, XBOOLE_0:def 4;

now :: thesis: for Y1 being set st Y1 in { ((downarrow x) /\ I) where I is Ideal of L : x <= sup I } holds
a in Y1

let Y1 be set ; :: thesis: ( Y1 in { ((downarrow x) /\ I) where I is Ideal of L : x <= sup I } implies a in Y1 )
assume Y1 in { ((downarrow x) /\ I) where I is Ideal of L : x <= sup I } ; :: thesis: a in Y1
then consider I1 being Ideal of L such that
A43: Y1 = (downarrow x) /\ I1 and
A44: x <= sup I1 ;
I1 in { I where I is Ideal of L : x <= sup I } by A44;
then a in I1 by A42, SETFAM_1:def 1;
hence a in Y1 by A41, A43, XBOOLE_0:def 4; :: thesis: verum

end;

hence a in meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I } by A6, A28, SETFAM_1:def 1; :: thesis: verum

end;

then (downarrow x) /\ (meet { I where I is Ideal of L : x <= sup I } ) = meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I } by A34;
then (downarrow x) /\ (waybelow x) = meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I } by Th34;
hence meet { ((DownMap I) . x) where I is Ideal of L : verum } = waybelow x by A33, WAYBEL_3:11, XBOOLE_1:28; :: thesis: verum

end;

end;