let L be complete LATTICE; :: thesis: for c1, c2 being closure Function of L,L holds
( c1 <= c2 iff Image c2 is SubRelStr of Image c1 )
let c1, c2 be closure Function of L,L; :: thesis: ( c1 <= c2 iff Image c2 is SubRelStr of Image c1 )
hereby :: thesis: ( Image c2 is SubRelStr of Image c1 implies c1 <= c2 )
assume A1: c1 <= c2 ; :: thesis: Image c2 is SubRelStr of Image c1
the carrier of (Image c2) c= the carrier of (Image c1)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (Image c2) or x in the carrier of (Image c1) )
assume x in the carrier of (Image c2) ; :: thesis: x in the carrier of (Image c1)
then consider y being Element of L such that
A2: c2 . y = x by YELLOW_2:10;
A3: c2 . (c2 . y) = c2 . y by YELLOW_2:18;
A4: c1 . (c2 . y) <= c2 . (c2 . y) by A1, YELLOW_2:9;
c2 . y <= c1 . (c2 . y) by Th5;
then c1 . (c2 . y) = x by A2, A4, A3, ORDERS_2:2;
then x in rng c1 by FUNCT_2:4;
hence x in the carrier of (Image c1) by YELLOW_0:def 15; :: thesis: verum
end;
hence Image c2 is SubRelStr of Image c1 by Th13; :: thesis: verum
end;
assume that
A5: the carrier of (Image c2) c= the carrier of (Image c1) and
the InternalRel of (Image c2) c= the InternalRel of (Image c1) ; :: according to YELLOW_0:def 13 :: thesis: c1 <= c2
now :: thesis: for x being Element of L holds c1 . x <= c2 . x
let x be Element of L; :: thesis: c1 . x <= c2 . x
c2 . x in rng c2 by FUNCT_2:4;
then c2 . x in the carrier of (Image c2) by YELLOW_0:def 15;
then ex a being Element of L st c1 . a = c2 . x by A5, YELLOW_2:10;
then A6: c1 . (c2 . x) = c2 . x by YELLOW_2:18;
x <= c2 . x by Th5;
hence c1 . x <= c2 . x by A6, WAYBEL_1:def 2; :: thesis: verum
end;
hence c1 <= c2 by YELLOW_2:9; :: thesis: verum