let L be lower-bounded continuous sup-Semilattice; :: thesis: for B being with_bottom CLbasis of L holds [(supMap (subrelstr B)),(baseMap B)] is Galois
let B be with_bottom CLbasis of L; :: thesis: [(supMap (subrelstr B)),(baseMap B)] is Galois

now

let x be Element of L; :: thesis: for y being Element of (InclPoset (Ids (subrelstr B))) holds
( ( x <= (supMap (subrelstr B)) . y implies (baseMap B) . x <= y ) & ( (baseMap B) . x <= y implies x <= (supMap (subrelstr B)) . y ) )
let y be Element of (InclPoset (Ids (subrelstr B))); :: thesis: ( ( x <= (supMap (subrelstr B)) . y implies (baseMap B) . x <= y ) & ( (baseMap B) . x <= y implies x <= (supMap (subrelstr B)) . y ) )
reconsider I = y as Ideal of (subrelstr B) by YELLOW_2:43;
reconsider J = I as non empty directed Subset of L by YELLOW_2:7;
A1: ( ex_sup_of J,L & ex_sup_of waybelow x,L & ex_sup_of downarrow J,L & ex_sup_of (waybelow x) /\ B,L ) by YELLOW_0:17;
thus ( x <= (supMap (subrelstr B)) . y implies (baseMap B) . x <= y ) :: thesis: ( (baseMap B) . x <= y implies x <= (supMap (subrelstr B)) . y )

proof

assume x <= (supMap (subrelstr B)) . y ; :: thesis: (baseMap B) . x <= y
then x <= "\/" I,L by Def10;
then A2: x <= sup (downarrow J) by A1, WAYBEL_0:33;
waybelow x c= downarrow J

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in waybelow x or z in downarrow J )
assume A3: z in waybelow x ; :: thesis: z in downarrow J
then reconsider z1 = z as Element of L ;
z1 << x by A3, WAYBEL_3:7;
hence z in downarrow J by A2, WAYBEL_3:20; :: thesis: verum

end;

then A4: (waybelow x) /\ B c= (downarrow J) /\ B by XBOOLE_1:26;
(downarrow J) /\ B c= J

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in (downarrow J) /\ B or z in J )
assume A5: z in (downarrow J) /\ B ; :: thesis: z in J
then A6: ( z in downarrow J & z in B ) by XBOOLE_0:def 4;
reconsider z1 = z as Element of L by A5;
reconsider z2 = z as Element of (subrelstr B) by A6, YELLOW_0:def 15;
consider v1 being Element of L such that
A7: v1 >= z1 and
A8: v1 in J by A6, WAYBEL_0:def 15;
reconsider v2 = v1 as Element of (subrelstr B) by A8;
z2 <= v2 by A7, YELLOW_0:61;
hence z in J by A8, WAYBEL_0:def 19; :: thesis: verum

end;

then (waybelow x) /\ B c= y by A4, XBOOLE_1:1;
then (baseMap B) . x c= y by Def12;
hence (baseMap B) . x <= y by YELLOW_1:3; :: thesis: verum

end;

thus ( (baseMap B) . x <= y implies x <= (supMap (subrelstr B)) . y ) :: thesis: verum

proof

assume (baseMap B) . x <= y ; :: thesis: x <= (supMap (subrelstr B)) . y
then (baseMap B) . x c= y by YELLOW_1:3;
then (waybelow x) /\ B c= y by Def12;
then sup ((waybelow x) /\ B) <= sup J by A1, YELLOW_0:34;
then x <= "\/" I,L by Def7;
hence x <= (supMap (subrelstr B)) . y by Def10; :: thesis: verum

end;

end;

hence [(supMap (subrelstr B)),(baseMap B)] is Galois by WAYBEL_1:9; :: thesis: verum