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;

subrelstr ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) is join-inheriting

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

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

A23:
subrelstr B is join-inheriting
by Def2;let y be Element of L; :: thesis: b_{1} = sup ((waybelow b_{1}) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)))

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

end;

suppose
not y <= "\/" (J,L)
; :: thesis: b_{1} = sup ((waybelow b_{1}) /\ ((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;

sup ((waybelow y) /\ B) is_>=_than (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))

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

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

A15:
(waybelow y) /\ B is_<=_than sup ((waybelow y) /\ B)
by YELLOW_0:32;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

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

hence
sup ((waybelow y) /\ B) <= b
by YELLOW_0:32; :: thesis: verum
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;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

sup ((waybelow y) /\ B) is_>=_than (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))

proof

then
sup ((waybelow y) /\ B) = sup ((waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)))
by A8, YELLOW_0:32;
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;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

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

suppose A18:
y <= "\/" (J,L)
; :: thesis: b_{1} = sup ((waybelow b_{1}) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)))

A19:
(waybelow y) /\ B c= (waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B))

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

(waybelow y) /\ ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) c= (waybelow y) /\ B
by A3, XBOOLE_1:26;
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;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

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

subrelstr ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)) is join-inheriting

proof

then A37:
(B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B) is join-closed
;
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;

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

hence
"\/" ({a,b},L) in the carrier of (subrelstr ((B \ J2) \/ ((waybelow ("\/" (J,L))) /\ B)))
by YELLOW_0:def 15; :: thesis: verumper 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;

end;

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 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;not a "\/" b in J

proof

then
not sup {a,b} in J
by YELLOW_0:41;
assume
a "\/" b in J
; :: thesis: contradiction

then a1 "\/" b1 in J1 by A23, YELLOW_0:70;

hence contradiction by A30, A32, WAYBEL_0:def 19; :: thesis: verum

end;then a1 "\/" b1 in J1 by A23, YELLOW_0:70;

hence contradiction by A30, A32, WAYBEL_0:def 19; :: thesis: verum

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

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 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;not a "\/" b in J

proof

then
not sup {a,b} in J
by YELLOW_0:41;
assume
a "\/" b in J
; :: thesis: contradiction

then a1 "\/" b1 in J1 by A23, YELLOW_0:70;

hence contradiction by A30, A33, WAYBEL_0:def 19; :: thesis: verum

end;then a1 "\/" b1 in J1 by A23, YELLOW_0:70;

hence contradiction by A30, A33, WAYBEL_0:def 19; :: thesis: verum

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

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 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;not a "\/" b in J

proof

then
not sup {a,b} in J
by YELLOW_0:41;
assume
a "\/" b in J
; :: thesis: contradiction

then a1 "\/" b1 in J1 by A23, YELLOW_0:70;

hence contradiction by A31, A34, WAYBEL_0:def 19; :: thesis: verum

end;then a1 "\/" b1 in J1 by A23, YELLOW_0:70;

hence contradiction by A31, A34, WAYBEL_0:def 19; :: thesis: verum

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

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

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

(waybelow ("\/" (J,L))) /\ B c= J
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;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

proof

hence
J = (waybelow ("\/" (J,L))) /\ B
by A40; :: thesis: verum
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;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