let L1, L2 be RelStr ; :: thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for X1 being Subset of L1

for X2 being Subset of L2 st X1 = X2 holds

( ( X1 is lower implies X2 is lower ) & ( X1 is upper implies X2 is upper ) ) )

assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; :: thesis: for X1 being Subset of L1

for X2 being Subset of L2 st X1 = X2 holds

( ( X1 is lower implies X2 is lower ) & ( X1 is upper implies X2 is upper ) )

let X1 be Subset of L1; :: thesis: for X2 being Subset of L2 st X1 = X2 holds

( ( X1 is lower implies X2 is lower ) & ( X1 is upper implies X2 is upper ) )

let X2 be Subset of L2; :: thesis: ( X1 = X2 implies ( ( X1 is lower implies X2 is lower ) & ( X1 is upper implies X2 is upper ) ) )

assume A2: X1 = X2 ; :: thesis: ( ( X1 is lower implies X2 is lower ) & ( X1 is upper implies X2 is upper ) )

A6: uparrow X1 = uparrow X2 by A1, A2, Th13;

uparrow X1 c= X1 by A5, Th24;

hence X2 is upper by A2, A6, Th24; :: thesis: verum

for X2 being Subset of L2 st X1 = X2 holds

( ( X1 is lower implies X2 is lower ) & ( X1 is upper implies X2 is upper ) ) )

assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; :: thesis: for X1 being Subset of L1

for X2 being Subset of L2 st X1 = X2 holds

( ( X1 is lower implies X2 is lower ) & ( X1 is upper implies X2 is upper ) )

let X1 be Subset of L1; :: thesis: for X2 being Subset of L2 st X1 = X2 holds

( ( X1 is lower implies X2 is lower ) & ( X1 is upper implies X2 is upper ) )

let X2 be Subset of L2; :: thesis: ( X1 = X2 implies ( ( X1 is lower implies X2 is lower ) & ( X1 is upper implies X2 is upper ) ) )

assume A2: X1 = X2 ; :: thesis: ( ( X1 is lower implies X2 is lower ) & ( X1 is upper implies X2 is upper ) )

hereby :: thesis: ( X1 is upper implies X2 is upper )

assume A5:
X1 is upper
; :: thesis: X2 is upper assume A3:
X1 is lower
; :: thesis: X2 is lower

A4: downarrow X1 = downarrow X2 by A1, A2, Th13;

downarrow X1 c= X1 by A3, Th23;

hence X2 is lower by A2, A4, Th23; :: thesis: verum

end;A4: downarrow X1 = downarrow X2 by A1, A2, Th13;

downarrow X1 c= X1 by A3, Th23;

hence X2 is lower by A2, A4, Th23; :: thesis: verum

A6: uparrow X1 = uparrow X2 by A1, A2, Th13;

uparrow X1 c= X1 by A5, Th24;

hence X2 is upper by A2, A6, Th24; :: thesis: verum