let L1 be non empty reflexive antisymmetric lower-bounded RelStr ; :: thesis: for L2 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete holds
the carrier of (CompactSublatt L1) = the carrier of (CompactSublatt L2)
let L2 be non empty reflexive antisymmetric RelStr ; :: thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete implies the carrier of (CompactSublatt L1) = the carrier of (CompactSublatt L2) )
assume that
A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and
A2: L1 is up-complete ; :: thesis: the carrier of (CompactSublatt L1) = the carrier of (CompactSublatt L2)
now :: thesis: for x being object st x in the carrier of (CompactSublatt L2) holds
x in the carrier of (CompactSublatt L1)
reconsider L29 = L2 as non empty reflexive antisymmetric lower-bounded RelStr by A1, YELLOW_0:13;
let x be object ; :: thesis: ( x in the carrier of (CompactSublatt L2) implies x in the carrier of (CompactSublatt L1) )
assume A3: x in the carrier of (CompactSublatt L2) ; :: thesis: x in the carrier of (CompactSublatt L1)
then x is Element of (CompactSublatt L29) ;
then reconsider x2 = x as Element of L2 by YELLOW_0:58;
reconsider x1 = x2 as Element of L1 by A1;
A4: x2 is compact by A3, WAYBEL_8:def 1;
L2 is up-complete by A1, A2, WAYBEL_8:15;
then x1 is compact by A1, A4, WAYBEL_8:9;
hence x in the carrier of (CompactSublatt L1) by WAYBEL_8:def 1; :: thesis: verum
end;
then A5: the carrier of (CompactSublatt L2) c= the carrier of (CompactSublatt L1) ;
now :: thesis: for x being object st x in the carrier of (CompactSublatt L1) holds
x in the carrier of (CompactSublatt L2)
let x be object ; :: thesis: ( x in the carrier of (CompactSublatt L1) implies x in the carrier of (CompactSublatt L2) )
assume A6: x in the carrier of (CompactSublatt L1) ; :: thesis: x in the carrier of (CompactSublatt L2)
then reconsider x1 = x as Element of L1 by YELLOW_0:58;
reconsider x2 = x1 as Element of L2 by A1;
x1 is compact by A6, WAYBEL_8:def 1;
then x2 is compact by A1, A2, WAYBEL_8:9;
hence x in the carrier of (CompactSublatt L2) by WAYBEL_8:def 1; :: thesis: verum
end;
then the carrier of (CompactSublatt L1) c= the carrier of (CompactSublatt L2) ;
hence the carrier of (CompactSublatt L1) = the carrier of (CompactSublatt L2) by A5, XBOOLE_0:def 10; :: thesis: verum