let L be lower-bounded continuous LATTICE; :: thesis: ( ex B being with_bottom CLbasis of L st

for B1 being with_bottom CLbasis of L holds B c= B1 implies L is algebraic )

given B being with_bottom CLbasis of L such that A1: for B1 being with_bottom CLbasis of L holds B c= B1 ; :: thesis: L is algebraic

A2: for x, y being Element of (InclPoset (Ids (subrelstr B))) holds

( x <= y iff (supMap (subrelstr B)) . x <= (supMap (subrelstr B)) . y )

then A8: baseMap B is onto by FUNCT_2:def 3;

[(supMap (subrelstr B)),(baseMap B)] is Galois by Th63;

then A9: supMap (subrelstr B) is V13() by A8, WAYBEL_1:27;

rng (supMap (subrelstr B)) = the carrier of L by Th65;

then supMap (subrelstr B) is isomorphic by A9, A2, WAYBEL_0:66;

then A10: InclPoset (Ids (subrelstr B)),L are_isomorphic by WAYBEL_1:def 8;

( InclPoset (Ids (subrelstr B)) is lower-bounded & InclPoset (Ids (subrelstr B)) is algebraic ) by WAYBEL13:10;

hence L is algebraic by A10, WAYBEL13:32; :: thesis: verum

for B1 being with_bottom CLbasis of L holds B c= B1 implies L is algebraic )

given B being with_bottom CLbasis of L such that A1: for B1 being with_bottom CLbasis of L holds B c= B1 ; :: thesis: L is algebraic

A2: for x, y being Element of (InclPoset (Ids (subrelstr B))) holds

( x <= y iff (supMap (subrelstr B)) . x <= (supMap (subrelstr B)) . y )

proof

the carrier of (InclPoset (Ids (subrelstr B))) c= rng (baseMap B)
let x, y be Element of (InclPoset (Ids (subrelstr B))); :: thesis: ( x <= y iff (supMap (subrelstr B)) . x <= (supMap (subrelstr B)) . y )

thus ( x <= y implies (supMap (subrelstr B)) . x <= (supMap (subrelstr B)) . y ) by WAYBEL_1:def 2; :: thesis: ( (supMap (subrelstr B)) . x <= (supMap (subrelstr B)) . y implies x <= y )

reconsider x1 = x, y1 = y as Ideal of (subrelstr B) by YELLOW_2:41;

assume A3: (supMap (subrelstr B)) . x <= (supMap (subrelstr B)) . y ; :: thesis: x <= y

A4: (supMap (subrelstr B)) . y1 = "\/" (y1,L) by Def10;

(supMap (subrelstr B)) . x1 = "\/" (x1,L) by Def10;

then waybelow ("\/" (x1,L)) c= waybelow ("\/" (y1,L)) by A4, A3, WAYBEL_3:25;

then A5: (waybelow ("\/" (x1,L))) /\ B c= (waybelow ("\/" (y1,L))) /\ B by XBOOLE_1:26;

A6: y = (waybelow ("\/" (y,L))) /\ B by A1, Th70;

x = (waybelow ("\/" (x,L))) /\ B by A1, Th70;

hence x <= y by A6, A5, YELLOW_1:3; :: thesis: verum

end;thus ( x <= y implies (supMap (subrelstr B)) . x <= (supMap (subrelstr B)) . y ) by WAYBEL_1:def 2; :: thesis: ( (supMap (subrelstr B)) . x <= (supMap (subrelstr B)) . y implies x <= y )

reconsider x1 = x, y1 = y as Ideal of (subrelstr B) by YELLOW_2:41;

assume A3: (supMap (subrelstr B)) . x <= (supMap (subrelstr B)) . y ; :: thesis: x <= y

A4: (supMap (subrelstr B)) . y1 = "\/" (y1,L) by Def10;

(supMap (subrelstr B)) . x1 = "\/" (x1,L) by Def10;

then waybelow ("\/" (x1,L)) c= waybelow ("\/" (y1,L)) by A4, A3, WAYBEL_3:25;

then A5: (waybelow ("\/" (x1,L))) /\ B c= (waybelow ("\/" (y1,L))) /\ B by XBOOLE_1:26;

A6: y = (waybelow ("\/" (y,L))) /\ B by A1, Th70;

x = (waybelow ("\/" (x,L))) /\ B by A1, Th70;

hence x <= y by A6, A5, YELLOW_1:3; :: thesis: verum

proof

then
rng (baseMap B) = the carrier of (InclPoset (Ids (subrelstr B)))
;
let J be object ; :: according to TARSKI:def 3 :: thesis: ( not J in the carrier of (InclPoset (Ids (subrelstr B))) or J in rng (baseMap B) )

reconsider JJ = J as set by TARSKI:1;

set x = "\/" (JJ,L);

assume J in the carrier of (InclPoset (Ids (subrelstr B))) ; :: thesis: J in rng (baseMap B)

then J = (waybelow ("\/" (JJ,L))) /\ B by A1, Th70;

then A7: J = (baseMap B) . ("\/" (JJ,L)) by Def12;

dom (baseMap B) = the carrier of L by FUNCT_2:def 1;

hence J in rng (baseMap B) by A7, FUNCT_1:def 3; :: thesis: verum

end;reconsider JJ = J as set by TARSKI:1;

set x = "\/" (JJ,L);

assume J in the carrier of (InclPoset (Ids (subrelstr B))) ; :: thesis: J in rng (baseMap B)

then J = (waybelow ("\/" (JJ,L))) /\ B by A1, Th70;

then A7: J = (baseMap B) . ("\/" (JJ,L)) by Def12;

dom (baseMap B) = the carrier of L by FUNCT_2:def 1;

hence J in rng (baseMap B) by A7, FUNCT_1:def 3; :: thesis: verum

then A8: baseMap B is onto by FUNCT_2:def 3;

[(supMap (subrelstr B)),(baseMap B)] is Galois by Th63;

then A9: supMap (subrelstr B) is V13() by A8, WAYBEL_1:27;

rng (supMap (subrelstr B)) = the carrier of L by Th65;

then supMap (subrelstr B) is isomorphic by A9, A2, WAYBEL_0:66;

then A10: InclPoset (Ids (subrelstr B)),L are_isomorphic by WAYBEL_1:def 8;

( InclPoset (Ids (subrelstr B)) is lower-bounded & InclPoset (Ids (subrelstr B)) is algebraic ) by WAYBEL13:10;

hence L is algebraic by A10, WAYBEL13:32; :: thesis: verum