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:43;
reconsider J2 = J1 as non empty directed Subset of L by YELLOW_2:7;
set x = "\/" J,L;
A2: (waybelow ("\/" J,L)) /\ B c= J

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (waybelow ("\/" J,L)) /\ B or a in J )
assume A3: a in (waybelow ("\/" J,L)) /\ B ; :: thesis: a in J
then A4: ( a in waybelow ("\/" J,L) & a in B ) by XBOOLE_0:def 4;
reconsider a1 = a as Element of L by A3;
reconsider a2 = a as Element of (subrelstr B) by A4, YELLOW_0:def 15;
a1 << "\/" J,L by A4, WAYBEL_3:7;
then consider d1 being Element of L such that
A5: d1 in J2 and
A6: a1 <= d1 by WAYBEL_3:def 1;
reconsider d2 = d1 as Element of (subrelstr B) by A5;
a2 <= d2 by A6, YELLOW_0:61;
hence a in J by A5, WAYBEL_0:def 19; :: thesis: verum

end;

set C = (B \ J2) \/ ((waybelow ("\/" J,L)) /\ B);
A7: B \ J2 c= B by XBOOLE_1:36;
(waybelow ("\/" J,L)) /\ B c= B by XBOOLE_1:17;
then A8: (B \ J2) \/ ((waybelow ("\/" J,L)) /\ B) c= B by A7, XBOOLE_1:8;
A9: 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
A10: a in the carrier of (subrelstr ((B \ J2) \/ ((waybelow ("\/" J,L)) /\ B))) and
A11: b in the carrier of (subrelstr ((B \ J2) \/ ((waybelow ("\/" J,L)) /\ B))) and
A12: ex_sup_of {a,b},L ; :: thesis: "\/" {a,b},L in the carrier of (subrelstr ((B \ J2) \/ ((waybelow ("\/" J,L)) /\ B)))
A13: ( a in (B \ J2) \/ ((waybelow ("\/" J,L)) /\ B) & b in (B \ J2) \/ ((waybelow ("\/" J,L)) /\ B) ) by A10, A11, YELLOW_0:def 15;
then reconsider a1 = a, b1 = b as Element of (subrelstr B) by A8, YELLOW_0:def 15;
A14: ( a1 <= a1 "\/" b1 & b1 <= a1 "\/" b1 ) by YELLOW_0:22;
A15: sup {a,b} in B by A8, A12, A13, Th16;

now

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 A13, 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 A16: not a in J by XBOOLE_0:def 5;
not a "\/" b in J

proof

assume a "\/" b in J ; :: thesis: contradiction
then a1 "\/" b1 in J1 by A9, YELLOW_0:71;
hence contradiction by A14, A16, WAYBEL_0:def 19; :: thesis: verum

end;

then not sup {a,b} in J by YELLOW_0:41;
then sup {a,b} in B \ J by A15, 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 A17: not a in J by XBOOLE_0:def 5;
not a "\/" b in J

proof

assume a "\/" b in J ; :: thesis: contradiction
then a1 "\/" b1 in J1 by A9, YELLOW_0:71;
hence contradiction by A14, A17, WAYBEL_0:def 19; :: thesis: verum

end;

then not sup {a,b} in J by YELLOW_0:41;
then sup {a,b} in B \ J by A15, 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 A18: not b in J by XBOOLE_0:def 5;
not a "\/" b in J

proof

assume a "\/" b in J ; :: thesis: contradiction
then a1 "\/" b1 in J1 by A9, YELLOW_0:71;
hence contradiction by A14, A18, WAYBEL_0:def 19; :: thesis: verum

end;

then not sup {a,b} in J by YELLOW_0:41;
then sup {a,b} in B \ J by A15, 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 (waybelow ("\/" J,L)) /\ B ) ; :: thesis: sup {a,b} in (B \ J2) \/ ((waybelow ("\/" J,L)) /\ B)

then ( a in waybelow ("\/" J,L) & b in waybelow ("\/" J,L) ) by XBOOLE_0:def 4;
then ( a << "\/" J,L & b << "\/" J,L ) by WAYBEL_3:7;
then a "\/" b << "\/" J,L by WAYBEL_3:3;
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 A15, XBOOLE_0:def 4;
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 A19: (B \ J2) \/ ((waybelow ("\/" J,L)) /\ B) is join-closed by Def2;

now

let y be Element of L; :: thesis: b₁ = sup ((waybelow b₁) /\ ((B \ J2) \/ ((waybelow ("\/" J,L)) /\ B)))

per cases ( not y <= "\/" J,L or y <= "\/" J,L ) ;

suppose not y <= "\/" J,L ; :: thesis: b₁ = sup ((waybelow b₁) /\ ((B \ J2) \/ ((waybelow ("\/" J,L)) /\ B)))

then consider u being Element of L such that
A20: u in B and
A21: not u <= "\/" J,L and
A22: u << y by Th46;
A23: (waybelow y) /\ B is_<=_than sup ((waybelow y) /\ B) by YELLOW_0:32;
A24: 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 b in (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" J,L)) /\ B)) ; :: thesis: b <= sup ((waybelow y) /\ B)
then ( b in waybelow y & b in (B \ J2) \/ ((waybelow ("\/" J,L)) /\ B) ) by XBOOLE_0:def 4;
then b in (waybelow y) /\ B by A8, XBOOLE_0:def 4;
hence b <= sup ((waybelow y) /\ B) by A23, LATTICE3:def 9; :: thesis: verum

end;

now

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 A25: 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 )
assume c in (waybelow y) /\ B ; :: thesis: c <= b
then A26: ( c in waybelow y & c in B ) by XBOOLE_0:def 4;
then c << y by WAYBEL_3:7;
then c "\/" u << y by A22, WAYBEL_3:3;
then A27: c "\/" u in waybelow y by WAYBEL_3:7;
sup {c,u} in B by A20, A26, Th18;
then A28: c "\/" u in B by YELLOW_0:41;
A29: J is_<=_than "\/" J,L by YELLOW_0:32;
u <= c "\/" u by YELLOW_0:22;
then not c "\/" u <= "\/" J,L by A21, YELLOW_0:def 2;
then not c "\/" u in J by A29, LATTICE3:def 9;
then c "\/" u in B \ J by A28, XBOOLE_0:def 5;
then c "\/" u in (B \ J2) \/ ((waybelow ("\/" J,L)) /\ B) by XBOOLE_0:def 3;
then c "\/" u in (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" J,L)) /\ B)) by A27, XBOOLE_0:def 4;
then A30: c "\/" u <= b by A25, LATTICE3:def 9;
c <= c "\/" u by YELLOW_0:22;
hence c <= b by A30, YELLOW_0:def 2; :: thesis: verum

end;

hence sup ((waybelow y) /\ B) <= b by YELLOW_0:32; :: thesis: verum

end;

then sup ((waybelow y) /\ B) = sup ((waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" J,L)) /\ B))) by A24, YELLOW_0:32;
hence y = sup ((waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" J,L)) /\ B))) by Def7; :: thesis: verum

end;

suppose A31: y <= "\/" J,L ; :: thesis: b₁ = sup ((waybelow b₁) /\ ((B \ J2) \/ ((waybelow ("\/" J,L)) /\ B)))

A32: (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" J,L)) /\ B)) c= (waybelow y) /\ B by A8, XBOOLE_1:26;
(waybelow y) /\ B c= (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" J,L)) /\ B))

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (waybelow y) /\ B or a in (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" J,L)) /\ B)) )
assume A33: a in (waybelow y) /\ B ; :: thesis: a in (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" J,L)) /\ B))
then A34: ( a in waybelow y & a in B ) by XBOOLE_0:def 4;
reconsider a1 = a as Element of L by A33;
a1 << y by A34, WAYBEL_3:7;
then a1 << "\/" J,L by A31, WAYBEL_3:2;
then a1 in waybelow ("\/" J,L) by WAYBEL_3:7;
then a in (waybelow ("\/" J,L)) /\ B by A34, 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 A34, XBOOLE_0:def 4; :: thesis: verum

end;

then (waybelow y) /\ B = (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" J,L)) /\ B)) by A32, XBOOLE_0:def 10;
hence y = sup ((waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" J,L)) /\ B))) by Def7; :: thesis: verum

end;

end;

end;

then reconsider C = (B \ J2) \/ ((waybelow ("\/" J,L)) /\ B) as CLbasis of L by A19, Def7;
A35: Bottom L in B by Def8;
Bottom L << "\/" J,L by WAYBEL_3:4;
then Bottom L in waybelow ("\/" J,L) by WAYBEL_3:7;
then Bottom L in (waybelow ("\/" J,L)) /\ B by A35, XBOOLE_0:def 4;
then Bottom L in C by XBOOLE_0:def 3;
then C is with_bottom by Def8;
then B c= C by A1;
then A36: B = C by A8, XBOOLE_0:def 10;
J c= (waybelow ("\/" J,L)) /\ B

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in J or a in (waybelow ("\/" J,L)) /\ B )
assume A37: a in J ; :: thesis: a in (waybelow ("\/" J,L)) /\ B
then a in J1 ;
then a in the carrier of (subrelstr B) ;
then A38: a in C by A36, YELLOW_0:def 15;
not a in B \ J2 by A37, XBOOLE_0:def 5;
hence a in (waybelow ("\/" J,L)) /\ B by A38, XBOOLE_0:def 3; :: thesis: verum

end;

hence J = (waybelow ("\/" J,L)) /\ B by A2, XBOOLE_0:def 10; :: thesis: verum