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 x1, y1 being Element of L1
for x2, y2 being Element of L2 st x1 = x2 & y1 = y2 & x1 << y1 holds
x2 << y2 )
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 x1, y1 being Element of L1
for x2, y2 being Element of L2 st x1 = x2 & y1 = y2 & x1 << y1 holds
x2 << y2
let x1, y1 be Element of L1; :: thesis: for x2, y2 being Element of L2 st x1 = x2 & y1 = y2 & x1 << y1 holds
x2 << y2
let x2, y2 be Element of L2; :: thesis: ( x1 = x2 & y1 = y2 & x1 << y1 implies x2 << y2 )
assume that
A3: x1 = x2 and
A4: y1 = y2 and
A5: x1 << y1 ; :: thesis: x2 << y2
now :: thesis: for D2 being non empty directed Subset of L2 st y2 <= sup D2 holds
ex d2 being Element of L2 st
( d2 in D2 & x2 <= d2 )
let D2 be non empty directed Subset of L2; :: thesis: ( y2 <= sup D2 implies ex d2 being Element of L2 st
( d2 in D2 & x2 <= d2 ) )
reconsider D1 = D2 as Subset of L1 by A1;
reconsider D1 = D1 as non empty directed Subset of L1 by A1, WAYBEL_0:3;
ex_sup_of D1,L1 by A2, WAYBEL_0:75;
then A6: sup D1 = sup D2 by A1, YELLOW_0:26;
assume y2 <= sup D2 ; :: thesis: ex d2 being Element of L2 st
( d2 in D2 & x2 <= d2 )
then y1 <= sup D1 by A1, A4, A6;
then consider d1 being Element of L1 such that
A7: d1 in D1 and
A8: x1 <= d1 by A5, WAYBEL_3:def 1;
reconsider d2 = d1 as Element of L2 by A1;
take d2 = d2; :: thesis: ( d2 in D2 & x2 <= d2 )
thus d2 in D2 by A7; :: thesis: x2 <= d2
thus x2 <= d2 by A1, A3, A8; :: thesis: verum
end;
hence x2 << y2 by WAYBEL_3:def 1; :: thesis: verum