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;
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

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
A5: u in B and
A6: not u <= "\/" J,L and
A7: u << y by Th46;

A8: 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 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, LATTICE3:def 9;
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, LATTICE3:def 9;
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, LATTICE3:def 9; :: 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: b₁ = sup ((waybelow b₁) /\ ((B \ J2) \/ ((waybelow ("\/" J,L)) /\ B)))

A19: (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 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, XBOOLE_0:def 10;
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

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

proof

assume a "\/" b in J ; :: thesis: contradiction
then a1 "\/" b1 in J1 by A23, YELLOW_0:71;
hence contradiction by A30, A32, 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 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

proof

assume a "\/" b in J ; :: thesis: contradiction
then a1 "\/" b1 in J1 by A23, YELLOW_0:71;
hence contradiction by A30, A33, 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 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

proof

assume a "\/" b in J ; :: thesis: contradiction
then a1 "\/" b1 in J1 by A23, YELLOW_0:71;
hence contradiction by A31, A34, 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 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 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 A35, XBOOLE_0:def 4;
then a << "\/" J,L by WAYBEL_3:7;
then a "\/" b << "\/" J,L by A36, 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 A29, 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 A37: (B \ J2) \/ ((waybelow ("\/" J,L)) /\ B) is join-closed by Def2;
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 by Def8;
then B c= C by A1;
then A39: B = C by A3, XBOOLE_0:def 10;
A40: 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 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 set ; :: 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:61;
hence a in J by A44, WAYBEL_0:def 19; :: thesis: verum

end;

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