let L1, L2 be non empty reflexive antisymmetric up-complete RelStr ; :: thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for x being Element of L1
for y being Element of L2 st x = y holds
compactbelow x = compactbelow y )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; :: thesis: for x being Element of L1
for y being Element of L2 st x = y holds
compactbelow x = compactbelow y
let x be Element of L1; :: thesis: for y being Element of L2 st x = y holds
compactbelow x = compactbelow y
let y be Element of L2; :: thesis: ( x = y implies compactbelow x = compactbelow y )
assume A2: x = y ; :: thesis: compactbelow x = compactbelow y
now :: thesis: for z being object st z in compactbelow y holds
z in compactbelow x
let z be object ; :: thesis: ( z in compactbelow y implies z in compactbelow x )
assume A3: z in compactbelow y ; :: thesis: z in compactbelow x
then reconsider z2 = z as Element of L2 ;
reconsider z1 = z2 as Element of L1 by A1;
z2 is compact by A3, Th4;
then A4: z1 is compact by A1, Th9;
z2 <= y by A3, Th4;
then z1 <= x by A1, A2;
hence z in compactbelow x by A4; :: thesis: verum
end;
then A5: compactbelow y c= compactbelow x ;
now :: thesis: for z being object st z in compactbelow x holds
z in compactbelow y
let z be object ; :: thesis: ( z in compactbelow x implies z in compactbelow y )
assume A6: z in compactbelow x ; :: thesis: z in compactbelow y
then reconsider z1 = z as Element of L1 ;
reconsider z2 = z1 as Element of L2 by A1;
z1 is compact by A6, Th4;
then A7: z2 is compact by A1, Th9;
z1 <= x by A6, Th4;
then z2 <= y by A1, A2;
hence z in compactbelow y by A7; :: thesis: verum
end;
then compactbelow x c= compactbelow y ;
hence compactbelow x = compactbelow y by A5, XBOOLE_0:def 10; :: thesis: verum