let L be lower-bounded continuous LATTICE; :: thesis: for B being with_bottom CLbasis of L st ( for B1 being with_bottom CLbasis of L holds B c= B1 ) holds
for J being Element of (InclPoset (Ids ())) holds J = (waybelow ("\/" (J,L))) /\ B

let B be with_bottom CLbasis of L; :: thesis: ( ( for B1 being with_bottom CLbasis of L holds B c= B1 ) implies for J being Element of (InclPoset (Ids ())) holds J = (waybelow ("\/" (J,L))) /\ B )
assume A1: for B1 being with_bottom CLbasis of L holds B c= B1 ; :: thesis: for J being Element of (InclPoset (Ids ())) holds J = (waybelow ("\/" (J,L))) /\ B
let J be Element of (InclPoset (Ids ())); :: thesis: J = (waybelow ("\/" (J,L))) /\ B
reconsider J1 = J as Ideal of () by YELLOW_2:41;
reconsider J2 = J1 as non empty directed Subset of L by YELLOW_2:7;
set x = "\/" (J,L);
set C = (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B);
A2: (waybelow ("\/" (J,L))) /\ B c= B by XBOOLE_1:17;
B \ J2 c= B by XBOOLE_1:36;
then A3: (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) c= B by ;
A4: now :: thesis: for y being Element of L holds y = sup (() /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)))
let y be Element of L; :: thesis: b1 = sup ((waybelow b1) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)))
per cases ( not y <= "\/" (J,L) or y <= "\/" (J,L) ) ;
suppose not y <= "\/" (J,L) ; :: thesis: b1 = sup ((waybelow b1) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)))
then consider u being Element of L such that
A5: u in B and
A6: not u <= "\/" (J,L) and
A7: u << y by Th46;
A8: now :: thesis: for b being Element of L st b is_>=_than () /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) holds
sup (() /\ B) <= b
let b be Element of L; :: thesis: ( b is_>=_than () /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) implies sup (() /\ B) <= b )
assume A9: b is_>=_than () /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) ; :: thesis: sup (() /\ B) <= b
b is_>=_than () /\ B
proof
let c be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not c in () /\ B or c <= b )
u <= c "\/" u by YELLOW_0:22;
then A10: not c "\/" u <= "\/" (J,L) by ;
assume A11: c in () /\ B ; :: thesis: c <= b
then c in B by XBOOLE_0:def 4;
then sup {c,u} in B by ;
then A12: c "\/" u in B by YELLOW_0:41;
J is_<=_than "\/" (J,L) by YELLOW_0:32;
then not c "\/" u in J by A10;
then c "\/" u in B \ J by ;
then A13: c "\/" u in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) by XBOOLE_0:def 3;
c in waybelow y by ;
then c << y by WAYBEL_3:7;
then c "\/" u << y by ;
then c "\/" u in waybelow y by WAYBEL_3:7;
then c "\/" u in () /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) by ;
then A14: c "\/" u <= b by A9;
c <= c "\/" u by YELLOW_0:22;
hence c <= b by ; :: thesis: verum
end;
hence sup (() /\ B) <= b by YELLOW_0:32; :: thesis: verum
end;
A15: (waybelow y) /\ B is_<=_than sup (() /\ B) by YELLOW_0:32;
sup (() /\ B) is_>=_than () /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))
proof
let b be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not b in () /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) or b <= sup (() /\ B) )
assume A16: b in () /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) ; :: thesis: b <= sup (() /\ B)
then A17: b in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) by XBOOLE_0:def 4;
b in waybelow y by ;
then b in () /\ B by ;
hence b <= sup (() /\ B) by A15; :: thesis: verum
end;
then sup (() /\ B) = sup (() /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))) by ;
hence y = sup (() /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))) by Def7; :: thesis: verum
end;
suppose A18: y <= "\/" (J,L) ; :: thesis: b1 = sup ((waybelow b1) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)))
A19: (waybelow y) /\ B c= () /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in () /\ B or a in () /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) )
assume A20: a in () /\ B ; :: thesis: a in () /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))
then reconsider a1 = a as Element of L ;
A21: a in waybelow y by ;
then a1 << y by WAYBEL_3:7;
then a1 << "\/" (J,L) by ;
then A22: a1 in waybelow ("\/" (J,L)) by WAYBEL_3:7;
a in B by ;
then a in (waybelow ("\/" (J,L))) /\ B by ;
then a in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) by XBOOLE_0:def 3;
hence a in () /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) by ; :: thesis: verum
end;
(waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) c= () /\ B by ;
then (waybelow y) /\ B = () /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) by A19;
hence y = sup (() /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))) by Def7; :: thesis: verum
end;
end;
end;
A23: subrelstr B is join-inheriting by Def2;
subrelstr ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) is join-inheriting
proof
let a, b be Element of L; :: according to YELLOW_0:def 17 :: thesis: ( not a in the carrier of (subrelstr ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))) or not b in the carrier of (subrelstr ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))) or not ex_sup_of {a,b},L or "\/" ({a,b},L) in the carrier of (subrelstr ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))) )
assume that
A24: a in the carrier of (subrelstr ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))) and
A25: b in the carrier of (subrelstr ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))) and
A26: ex_sup_of {a,b},L ; :: thesis: "\/" ({a,b},L) in the carrier of (subrelstr ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)))
A27: b in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) by ;
A28: a in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) by ;
then A29: sup {a,b} in B by A3, A26, A27, Th16;
reconsider a1 = a, b1 = b as Element of () by ;
A30: a1 <= a1 "\/" b1 by YELLOW_0:22;
A31: b1 <= a1 "\/" b1 by YELLOW_0:22;
now :: thesis: sup {a,b} in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)
per cases ( ( a in B \ J & b in B \ J ) or ( a in B \ J & b in (waybelow ("\/" (J,L))) /\ B ) or ( a in (waybelow ("\/" (J,L))) /\ B & b in B \ J ) or ( a in (waybelow ("\/" (J,L))) /\ B & b in (waybelow ("\/" (J,L))) /\ B ) ) by ;
suppose ( a in B \ J & b in B \ J ) ; :: thesis: sup {a,b} in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)
end;
suppose ( a in B \ J & b in (waybelow ("\/" (J,L))) /\ B ) ; :: thesis: sup {a,b} in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)
end;
suppose ( a in (waybelow ("\/" (J,L))) /\ B & b in B \ J ) ; :: thesis: sup {a,b} in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)
end;
suppose A35: ( a in (waybelow ("\/" (J,L))) /\ B & b in (waybelow ("\/" (J,L))) /\ B ) ; :: thesis: sup {a,b} in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)
then b in waybelow ("\/" (J,L)) by XBOOLE_0:def 4;
then A36: b << "\/" (J,L) by WAYBEL_3:7;
a in waybelow ("\/" (J,L)) by ;
then a << "\/" (J,L) by WAYBEL_3:7;
then a "\/" b << "\/" (J,L) by ;
then a "\/" b in waybelow ("\/" (J,L)) by WAYBEL_3:7;
then sup {a,b} in waybelow ("\/" (J,L)) by YELLOW_0:41;
then sup {a,b} in (waybelow ("\/" (J,L))) /\ B by ;
hence sup {a,b} in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
hence "\/" ({a,b},L) in the carrier of (subrelstr ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))) by YELLOW_0:def 15; :: thesis: verum
end;
then A37: (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) is join-closed ;
Bottom L << "\/" (J,L) by WAYBEL_3:4;
then A38: Bottom L in waybelow ("\/" (J,L)) by WAYBEL_3:7;
reconsider C = (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) as CLbasis of L by ;
Bottom L in B by Def8;
then Bottom L in (waybelow ("\/" (J,L))) /\ B by ;
then Bottom L in C by XBOOLE_0:def 3;
then C is with_bottom ;
then B c= C by A1;
then A39: B = C by A3;
A40: J c= (waybelow ("\/" (J,L))) /\ B
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in J or a in (waybelow ("\/" (J,L))) /\ B )
assume A41: a in J ; :: thesis: a in (waybelow ("\/" (J,L))) /\ B
then a in J1 ;
then a in the carrier of () ;
then A42: a in C by ;
not a in B \ J2 by ;
hence a in (waybelow ("\/" (J,L))) /\ B by ; :: thesis: verum
end;
(waybelow ("\/" (J,L))) /\ B c= J
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (waybelow ("\/" (J,L))) /\ B or a in J )
assume A43: a in (waybelow ("\/" (J,L))) /\ B ; :: thesis: a in J
then reconsider a1 = a as Element of L ;
a in B by ;
then reconsider a2 = a as Element of () by YELLOW_0:def 15;
a in waybelow ("\/" (J,L)) by ;
then a1 << "\/" (J,L) by WAYBEL_3:7;
then consider d1 being Element of L such that
A44: d1 in J2 and
A45: a1 <= d1 by WAYBEL_3:def 1;
reconsider d2 = d1 as Element of () by A44;
a2 <= d2 by ;
hence a in J by ; :: thesis: verum
end;
hence J = (waybelow ("\/" (J,L))) /\ B by A40; :: thesis: verum