let L be lower-bounded continuous sup-Semilattice; :: thesis: for B being with_bottom CLbasis of L holds [(supMap ()),()] is Galois
let B be with_bottom CLbasis of L; :: thesis: [(supMap ()),()] is Galois
now :: thesis: for x being Element of L
for y being Element of (InclPoset (Ids ())) holds
( ( x <= (supMap ()) . y implies () . x <= y ) & ( () . x <= y implies x <= (supMap ()) . y ) )
let x be Element of L; :: thesis: for y being Element of (InclPoset (Ids ())) holds
( ( x <= (supMap ()) . y implies () . x <= y ) & ( () . x <= y implies x <= (supMap ()) . y ) )

let y be Element of (InclPoset (Ids ())); :: thesis: ( ( x <= (supMap ()) . y implies () . x <= y ) & ( () . x <= y implies x <= (supMap ()) . y ) )
reconsider I = y as Ideal of () by YELLOW_2:41;
reconsider J = I as non empty directed Subset of L by YELLOW_2:7;
A1: ex_sup_of () /\ B,L by YELLOW_0:17;
thus ( x <= (supMap ()) . y implies () . x <= y ) :: thesis: ( () . x <= y implies x <= (supMap ()) . y )
proof
A2: (downarrow J) /\ B c= J
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in () /\ B or z in J )
assume A3: z in () /\ B ; :: thesis: z in J
then reconsider z1 = z as Element of L ;
z in B by ;
then reconsider z2 = z as Element of () by YELLOW_0:def 15;
z in downarrow J by ;
then consider v1 being Element of L such that
A4: v1 >= z1 and
A5: v1 in J by WAYBEL_0:def 15;
reconsider v2 = v1 as Element of () by A5;
z2 <= v2 by ;
hence z in J by ; :: thesis: verum
end;
assume x <= (supMap ()) . y ; :: thesis: () . x <= y
then x <= "\/" (I,L) by Def10;
then A6: x <= sup () by ;
waybelow x c= downarrow J
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in waybelow x or z in downarrow J )
assume A7: z in waybelow x ; :: thesis:
then reconsider z1 = z as Element of L ;
z1 << x by ;
hence z in downarrow J by ; :: thesis: verum
end;
then (waybelow x) /\ B c= () /\ B by XBOOLE_1:26;
then (waybelow x) /\ B c= y by A2;
then (baseMap B) . x c= y by Def12;
hence (baseMap B) . x <= y by YELLOW_1:3; :: thesis: verum
end;
A8: ex_sup_of J,L by YELLOW_0:17;
thus ( (baseMap B) . x <= y implies x <= (supMap ()) . y ) :: thesis: verum
proof
assume (baseMap B) . x <= y ; :: thesis: x <= (supMap ()) . y
then (baseMap B) . x c= y by YELLOW_1:3;
then (waybelow x) /\ B c= y by Def12;
then sup (() /\ B) <= sup J by ;
then x <= "\/" (I,L) by Def7;
hence x <= (supMap ()) . y by Def10; :: thesis: verum
end;
end;
hence [(supMap ()),()] is Galois by WAYBEL_1:8; :: thesis: verum