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 } = { ((downarrow x) /\ I) where I is Ideal of L : x <= sup I }

proof

thus { ((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 } :: according to XBOOLE_0:def 10 :: thesis: { ((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 set ; :: 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 & x <= sup I1 ) ;
a = (downarrow x) /\ I1 by A2, Def17;
hence a in { ((downarrow x) /\ I) where I is Ideal of L : x <= sup I } by A2; :: thesis: verum

end;

thus { ((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 } :: thesis: verum

proof

let a be set ; :: 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
A3: ( a = (downarrow x) /\ I1 & x <= sup I1 ) ;
a = (DownMap I1) . x by A3, Def17;
hence a in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } by A3; :: thesis: verum

end;

end;

set A2 = { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } ;
A4: { ((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 }

proof

thus { ((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 } :: according to XBOOLE_0:def 10 :: thesis: { (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 set ; :: 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 consider I1 being Ideal of L such that
A5: ( a = (DownMap I1) . x & not x <= sup I1 ) ;
a = downarrow x by A5, Def17;
hence a in { (downarrow x) where I is Ideal of L : not x <= sup I } by A5; :: thesis: verum

end;

thus { (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 } :: thesis: verum

proof

let a be set ; :: 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
A6: ( a = downarrow x & not x <= sup I1 ) ;
a = (DownMap I1) . x by A6, Def17;
hence a in { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } by A6; :: thesis: verum

end;

end;

A7: { ((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 }

proof

thus { ((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 } :: according to XBOOLE_0:def 10 :: thesis: { ((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 set ; :: 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
A8: 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 A8;
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;

thus { ((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 } :: thesis: verum

proof

let a be set ; :: 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
A9: ( ( 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 A9;

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;

end;

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

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

A11: { ((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 A2' = { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } as non empty set ;
consider a being Element of A2';
a in A2' ;
then consider I1 being Ideal of L such that
A12: ( a = downarrow x & not x <= sup I1 ) by A4;
thus contradiction by A10, A12, YELLOW_0:44; :: thesis: verum

end;

set Dx = downarrow x;
x <= sup (downarrow x) by A10, YELLOW_0:44;
then A13: (downarrow x) /\ (downarrow x) in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } by A1;
{ ((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 set ; :: 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 consider H being Ideal of L such that
A14: ( a = (downarrow x) /\ H & x <= sup H ) by A1;
reconsider a' = a as Ideal of L by A14, YELLOW_2:42;
x <= sup a' by A10, YELLOW_0:44;
hence a in { K where K is Ideal of L : x <= sup K } ; :: thesis: verum

end;

then A15: 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 A13, SETFAM_1:7;
A16: meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I } = {x}

proof

reconsider I' = downarrow x as Ideal of L ;
x <= sup I' by A10, YELLOW_0:44;
then (downarrow x) /\ I' in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } by A1;
then {x} in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } by A10, Th23;
hence meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I } c= {x} by SETFAM_1:4; :: 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 Z1' being Ideal of L such that
A17: ( Z1 = (downarrow x) /\ Z1' & x <= sup Z1' ) by A1;
A18: {x} c= Z1' by A10, Lm4;
{x} c= downarrow x by A10, Th23;
hence {x} c= Z1 by A17, A18, XBOOLE_1:19; :: thesis: verum

end;

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

end;

consider E being Ideal of L;
x <= sup E by A10, YELLOW_0:44;
then A19: E 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 consider K1 being Ideal of L such that
A20: ( K1 = Z1 & x <= sup K1 ) ;
thus meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I } c= Z1 by A10, 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 A19, SETFAM_1:6;
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 A15, XBOOLE_0:def 10;
hence meet { ((DownMap I) . x) where I is Ideal of L : verum } = waybelow x by A7, A11, Th34; :: thesis: verum

end;

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

set O = downarrow (Bottom L);
A22: sup (downarrow (Bottom L)) = Bottom L by WAYBEL_0:34;
then not x < sup (downarrow (Bottom L)) by ORDERS_2:30, YELLOW_0:44;
then not x <= sup (downarrow (Bottom L)) by A21, A22, ORDERS_2:def 10;
then A23: downarrow x in { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } by A4;
reconsider O1 = downarrow x as Ideal of L ;
A24: x <= sup O1 by WAYBEL_0:34;
downarrow x = (downarrow x) /\ O1 ;
then A25: ( downarrow x in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } & downarrow x in { (downarrow x) where I is Ideal of L : x <= sup I } ) by A1, A24;
A26: meet { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } = downarrow x

proof

thus meet { ((DownMap I) . x) where I is Ideal of L : not x <= sup I } c= downarrow x by A23, SETFAM_1:4; :: according to XBOOLE_0:def 10 :: thesis: downarrow x c= meet { ((DownMap I) . x) where I is Ideal of L : not x <= sup I }

now

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 consider L1 being Ideal of L such that
A27: ( Z1 = downarrow x & not x <= sup L1 ) by A4;
thus downarrow x c= Z1 by A27; :: thesis: verum

end;

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

end;

A28: 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 A7, A23, A25, SETFAM_1:10;
A29: meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I } c= downarrow x by A25, SETFAM_1:4;
A30: 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 A25, A26, A28, SETFAM_1:4, XBOOLE_1:28;
A31: 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 set ; :: 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 A32: 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 L' = [#] L as Subset of L ;
ex_sup_of L',L by YELLOW_0:17;
then L' is_<=_than sup L' by YELLOW_0:def 9;
then x <= sup L' by LATTICE3:def 9;
then A34: L' in { I where I is Ideal of L : x <= sup I } ;
a in meet { I where I is Ideal of L : x <= sup I }

proof

now

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 Y1' being Ideal of L such that
A35: ( Y1 = Y1' & x <= sup Y1' ) ;
A36: (downarrow x) /\ Y1' c= Y1' by XBOOLE_1:17;
(downarrow x) /\ Y1' in { ((DownMap I) . x) where I is Ideal of L : x <= sup I } by A1, A35;
then a in (downarrow x) /\ Y1' by A32, SETFAM_1:def 1;
hence a in Y1 by A35, A36; :: thesis: verum

end;

hence a in meet { I where I is Ideal of L : x <= sup I } by A34, SETFAM_1:def 1; :: thesis: verum

end;

hence a in (downarrow x) /\ (meet { I where I is Ideal of L : x <= sup I } ) by A29, A32, 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 set ; :: 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 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 A37: ( a in downarrow x & a in meet { I where I is Ideal of L : x <= sup I } ) by XBOOLE_0:def 4;
thus a in meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I } :: thesis: verum

proof

now

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
A38: ( Y1 = (downarrow x) /\ I1 & x <= sup I1 ) ;
I1 in { I where I is Ideal of L : x <= sup I } by A38;
then a in I1 by A37, SETFAM_1:def 1;
hence a in Y1 by A37, A38, XBOOLE_0:def 4; :: thesis: verum

end;

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

end;

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 A31, XBOOLE_0:def 10;
then A39: (downarrow x) /\ (waybelow x) = meet { ((DownMap I) . x) where I is Ideal of L : x <= sup I } by Th34;
waybelow x c= downarrow x by WAYBEL_3:11;
hence meet { ((DownMap I) . x) where I is Ideal of L : verum } = waybelow x by A30, A39, XBOOLE_1:28; :: thesis: verum

end;

end;