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 :: thesis: for x being Element of L
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 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:41;
reconsider J = I as non empty directed Subset of L by YELLOW_2:7;
A1: 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

A2: (downarrow J) /\ B c= J

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in (downarrow J) /\ B or z in J )
assume A3: z in (downarrow J) /\ B ; :: thesis: z in J
then reconsider z1 = z as Element of L ;
z in B by A3, XBOOLE_0:def 4;
then reconsider z2 = z as Element of (subrelstr B) by YELLOW_0:def 15;
z in downarrow J by A3, XBOOLE_0:def 4;
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 (subrelstr B) by A5;
z2 <= v2 by A4, YELLOW_0:60;
hence z in J by A5, WAYBEL_0:def 19; :: thesis: verum

end;

assume x <= (supMap (subrelstr B)) . y ; :: thesis: (baseMap B) . x <= y
then x <= "\/" (I,L) by Def10;
then A6: x <= sup (downarrow J) by WAYBEL_0:33, YELLOW_0:17;
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: z in downarrow J
then reconsider z1 = z as Element of L ;
z1 << x by A7, WAYBEL_3:7;
hence z in downarrow J by A6, WAYBEL_3:20; :: thesis: verum

end;

then (waybelow x) /\ B c= (downarrow J) /\ 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 (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 A8, 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:8; :: thesis: verum