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 (subrelstr B))) 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 (subrelstr B))) 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 (subrelstr B))) holds J = (waybelow ("\/" (J,L))) /\ B
let J be Element of (InclPoset (Ids (subrelstr B))); :: thesis: J = (waybelow ("\/" (J,L))) /\ B
reconsider J1 = J as Ideal of (subrelstr B) 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 A2, XBOOLE_1:8;
A4: now :: thesis: for y being Element of L holds y = sup ((waybelow y) /\ ((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 (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) holds
sup ((waybelow y) /\ B) <= b
let b be Element of L; :: thesis: ( b is_>=_than (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) implies sup ((waybelow y) /\ B) <= b )
assume A9: b is_>=_than (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) ; :: thesis: sup ((waybelow y) /\ B) <= b
b is_>=_than (waybelow y) /\ B
proof
let c be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not c in (waybelow y) /\ B or c <= b )
u <= c "\/" u by YELLOW_0:22;
then A10: not c "\/" u <= "\/" (J,L) by A6, YELLOW_0:def 2;
assume A11: c in (waybelow y) /\ B ; :: thesis: c <= b
then c in B by XBOOLE_0:def 4;
then sup {c,u} in B by A5, Th18;
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 A12, XBOOLE_0:def 5;
then A13: c "\/" u in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) by XBOOLE_0:def 3;
c in waybelow y by A11, XBOOLE_0:def 4;
then c << y by WAYBEL_3:7;
then c "\/" u << y by A7, WAYBEL_3:3;
then c "\/" u in waybelow y by WAYBEL_3:7;
then c "\/" u in (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) by A13, XBOOLE_0:def 4;
then A14: c "\/" u <= b by A9;
c <= c "\/" u by YELLOW_0:22;
hence c <= b by A14, YELLOW_0:def 2; :: thesis: verum
end;
hence sup ((waybelow y) /\ B) <= b by YELLOW_0:32; :: thesis: verum
end;
A15: (waybelow y) /\ B is_<=_than sup ((waybelow y) /\ B) by YELLOW_0:32;
sup ((waybelow y) /\ B) is_>=_than (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))
proof
let b be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not b in (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) or b <= sup ((waybelow y) /\ B) )
assume A16: b in (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) ; :: thesis: b <= sup ((waybelow y) /\ B)
then A17: b in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) by XBOOLE_0:def 4;
b in waybelow y by A16, XBOOLE_0:def 4;
then b in (waybelow y) /\ B by A3, A17, XBOOLE_0:def 4;
hence b <= sup ((waybelow y) /\ B) by A15; :: thesis: verum
end;
then sup ((waybelow y) /\ B) = sup ((waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))) by A8, YELLOW_0:32;
hence y = sup ((waybelow y) /\ ((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= (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (waybelow y) /\ B or a in (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) )
assume A20: a in (waybelow y) /\ B ; :: thesis: a in (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))
then reconsider a1 = a as Element of L ;
A21: a in waybelow y by A20, XBOOLE_0:def 4;
then a1 << y by WAYBEL_3:7;
then a1 << "\/" (J,L) by A18, WAYBEL_3:2;
then A22: a1 in waybelow ("\/" (J,L)) by WAYBEL_3:7;
a in B by A20, XBOOLE_0:def 4;
then a in (waybelow ("\/" (J,L))) /\ B by A22, XBOOLE_0:def 4;
then a in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) by XBOOLE_0:def 3;
hence a in (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) by A21, XBOOLE_0:def 4; :: thesis: verum
end;
(waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) c= (waybelow y) /\ B by A3, XBOOLE_1:26;
then (waybelow y) /\ B = (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) by A19;
hence y = sup ((waybelow y) /\ ((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 A25, YELLOW_0:def 15;
A28: a in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) by A24, YELLOW_0:def 15;
then A29: sup {a,b} in B by A3, A26, A27, Th16;
reconsider a1 = a, b1 = b as Element of (subrelstr B) by A3, A28, A27, YELLOW_0:def 15;
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 A28, A27, XBOOLE_0:def 3;
suppose ( a in B \ J & b in B \ J ) ; :: thesis: sup {a,b} in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)
then A32: not a in J by XBOOLE_0:def 5;
not a "\/" b in J then not sup {a,b} in J by YELLOW_0:41;
then sup {a,b} in B \ J by A29, XBOOLE_0:def 5;
hence sup {a,b} in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) by XBOOLE_0:def 3; :: thesis: verum
end;
suppose ( a in B \ J & b in (waybelow ("\/" (J,L))) /\ B ) ; :: thesis: sup {a,b} in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)
then A33: not a in J by XBOOLE_0:def 5;
not a "\/" b in J then not sup {a,b} in J by YELLOW_0:41;
then sup {a,b} in B \ J by A29, XBOOLE_0:def 5;
hence sup {a,b} in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) by XBOOLE_0:def 3; :: thesis: verum
end;
suppose ( a in (waybelow ("\/" (J,L))) /\ B & b in B \ J ) ; :: thesis: sup {a,b} in (B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)
then A34: not b in J by XBOOLE_0:def 5;
not a "\/" b in J then not sup {a,b} in J by YELLOW_0:41;
then sup {a,b} in B \ J by A29, XBOOLE_0:def 5;
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 A37, A4, Def7;
Bottom L in B by Def8;
then Bottom L in (waybelow ("\/" (J,L))) /\ B by A38, XBOOLE_0:def 4;
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 (subrelstr B) ;
then A42: a in C by A39, YELLOW_0:def 15;
not a in B \ J2 by A41, XBOOLE_0:def 5;
hence a in (waybelow ("\/" (J,L))) /\ B by A42, XBOOLE_0:def 3; :: 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 A43, XBOOLE_0:def 4;
then reconsider a2 = a as Element of (subrelstr B) by YELLOW_0:def 15;
a in waybelow ("\/" (J,L)) by A43, XBOOLE_0:def 4;
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 (subrelstr B) by A44;
a2 <= d2 by A45, YELLOW_0:60;
hence a in J by A44, WAYBEL_0:def 19; :: thesis: verum
end;
hence J = (waybelow ("\/" (J,L))) /\ B by A40; :: thesis: verum