let L1, 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 for x being Element of L1
for y being Element of L2 st x = y & x is compact holds
y is compact )
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: for x being Element of L1
for y being Element of L2 st x = y & x is compact holds
y is compact
let x be Element of L1; :: thesis: for y being Element of L2 st x = y & x is compact holds
y is compact
let y be Element of L2; :: thesis: ( x = y & x is compact implies y is compact )
assume that
A3: x = y and
A4: x is compact ; :: thesis: y is compact
x << x by A4, WAYBEL_3:def 2;
then y << y by A1, A2, A3, Th8;
hence y is compact by WAYBEL_3:def 2; :: thesis: verum