let L be non empty complete Poset; :: thesis: ( [(IdsMap L),(SupMap L)] is Galois & SupMap L is sups-preserving )
set g = IdsMap L;
set d = SupMap L;
now :: thesis: for I being Element of (InclPoset (Ids L))
for x being Element of L holds
( ( I <= (IdsMap L) . x implies (SupMap L) . I <= x ) & ( (SupMap L) . I <= x implies I <= (IdsMap L) . x ) )
let I be Element of (InclPoset (Ids L)); :: thesis: for x being Element of L holds
( ( I <= (IdsMap L) . x implies (SupMap L) . I <= x ) & ( (SupMap L) . I <= x implies I <= (IdsMap L) . x ) )
let x be Element of L; :: thesis: ( ( I <= (IdsMap L) . x implies (SupMap L) . I <= x ) & ( (SupMap L) . I <= x implies I <= (IdsMap L) . x ) )
reconsider I9 = I as Ideal of L by YELLOW_2:41;
hereby :: thesis: ( (SupMap L) . I <= x implies I <= (IdsMap L) . x )
assume I <= (IdsMap L) . x ; :: thesis: (SupMap L) . I <= x
then I c= (IdsMap L) . x by YELLOW_1:3;
then I9 c= downarrow x by YELLOW_2:def 4;
then x is_>=_than I9 by YELLOW_2:1;
then sup I9 <= x by YELLOW_0:32;
hence (SupMap L) . I <= x by YELLOW_2:def 3; :: thesis: verum
end;
assume (SupMap L) . I <= x ; :: thesis: I <= (IdsMap L) . x
then A1: sup I9 <= x by YELLOW_2:def 3;
sup I9 is_>=_than I9 by YELLOW_0:32;
then x is_>=_than I9 by A1, YELLOW_0:4;
then I9 c= downarrow x by YELLOW_2:1;
then I c= (IdsMap L) . x by YELLOW_2:def 4;
hence I <= (IdsMap L) . x by YELLOW_1:3; :: thesis: verum
end;
hence [(IdsMap L),(SupMap L)] is Galois ; :: thesis: SupMap L is sups-preserving
then SupMap L is lower_adjoint ;
hence SupMap L is sups-preserving ; :: thesis: verum