let L1, L2 be non empty reflexive 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 L2 is up-complete )
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: L2 is up-complete

now

let X be non empty directed Subset of ; :: thesis: ex x being Element of st
( x is_>=_than X & ( for y being Element of st y is_>=_than X holds
x <= y ) )
reconsider X' = X as Subset of by A1;
reconsider X' = X' as non empty directed Subset of by A1, WAYBEL_0:3;
consider x' being Element of such that
A3: x' is_>=_than X' and
A4: for y' being Element of st y' is_>=_than X' holds
x' <= y' by A2, WAYBEL_0:def 39;
reconsider x = x' as Element of by A1;
take x = x; :: thesis: ( x is_>=_than X & ( for y being Element of st y is_>=_than X holds
x <= y ) )
thus x is_>=_than X by A1, A3, YELLOW_0:2; :: thesis: for y being Element of st y is_>=_than X holds
x <= y
let y be Element of ; :: thesis: ( y is_>=_than X implies x <= y )
assume A5: y is_>=_than X ; :: thesis: x <= y
reconsider y' = y as Element of by A1;
x' <= y' by A1, A4, A5, YELLOW_0:2;
hence x <= y by A1, YELLOW_0:1; :: thesis: verum

end;

hence L2 is up-complete by WAYBEL_0:def 39; :: thesis: verum