let S, T be non empty reflexive RelStr ; :: thesis: ( RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) & S is /\-complete implies T is /\-complete )
assume that
A1: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) and
A2: for X being non empty Subset of S ex x being Element of S st
( x is_<=_than X & ( for y being Element of S st y is_<=_than X holds
x >= y ) ) ; :: according to WAYBEL_0:def 40 :: thesis: T is /\-complete
let X be non empty Subset of T; :: according to WAYBEL_0:def 40 :: thesis: ex b₁ being M3( the carrier of T) st
( b₁ is_<=_than X & ( for b₂ being M3( the carrier of T) holds
( not b₂ is_<=_than X or b₂ <= b₁ ) ) )
consider x being Element of S such that
A3: x is_<=_than X and
A4: for y being Element of S st y is_<=_than X holds
x >= y by A1, A2;
reconsider z = x as Element of T by A1;
take z ; :: thesis: ( z is_<=_than X & ( for b₁ being M3( the carrier of T) holds
( not b₁ is_<=_than X or b₁ <= z ) ) )
thus z is_<=_than X by A1, A3, YELLOW_0:2; :: thesis: for b₁ being M3( the carrier of T) holds
( not b₁ is_<=_than X or b₁ <= z )
let y be Element of T; :: thesis: ( not y is_<=_than X or y <= z )
reconsider s = y as Element of S by A1;
assume y is_<=_than X ; :: thesis: y <= z
then x >= s by A1, A4, YELLOW_0:2;
hence y <= z by A1, YELLOW_0:1; :: thesis: verum